| import Lean | |
| open Lean Elab | |
| declare_syntax_cat fixDecl | |
| syntax ident : fixDecl | |
| syntax ident "<" term : fixDecl | |
| syntax "Fix₁ " fixDecl : tactic | |
| elab_rules : tactic | |
| | `(tactic| Fix₁ $x:ident) => logInfo "simple" | |
| elab_rules : tactic | |
| | `(tactic| Fix₁ $x:ident < $bound:term) => | |
| throwError "Failed at elab_rules" | |
| macro_rules | |
| | `(ℕ) => `(Nat) | |
| example : ∀ b : ℕ, ∀ a : Nat, a ≥ 2 → a / a = 1 := by | |
| Fix₁ b | |
| Fix₁ a < 2 -- should produce `Failed at elab_rules` |