| example : True := by | |
| skip | |
| skip --< should complain about misleading indentation | |
| trivial | |
| macro "frobnicate" : tactic => `(tactic| skip) | |
| example : True := by | |
| conv => | |
| skip | |
| frobnicate --< should not parse frobnicate as a tactic | |
| trivial | |
| -- check error message without default handler for conv tactics | |
| declare_syntax_cat item | |
| syntax "valid_item" : item | |
| macro "block" "=>" sepByIndentSemicolon(item) : tactic => `(tactic| skip) | |
| example : True := by | |
| block => | |
| valid_item | |
| frobnicate --< should not parse frobnicate as a tactic |