From 2cb333a26000360be75181c16f26cdc889a822b1 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sun, 13 Nov 2022 22:57:22 -0500 Subject: [PATCH] feat: `elab_rules : conv` --- src/Lean/Elab/ElabRules.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean index c51c7bcf96..a47bab0bfc 100644 --- a/src/Lean/Elab/ElabRules.lean +++ b/src/Lean/Elab/ElabRules.lean @@ -67,7 +67,7 @@ def elabElabRulesAux (doc? : Option (TSyntax ``docComment)) `($[$doc?:docComment]? @[$(← mkAttrs `command_elab),*] aux_def elabRules $(mkIdent k) : Lean.Elab.Command.CommandElab := fun $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax) - else if catName == `tactic then + else if catName == `tactic || catName == `conv then `($[$doc?:docComment]? @[$(← mkAttrs `tactic),*] aux_def elabRules $(mkIdent k) : Lean.Elab.Tactic.Tactic := fun $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax)