max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: elab_rules : conv

Browse source
This commit is contained in:
Mario Carneiro 2022-11-13 22:57:22 -05:00 • committed by Leonardo de Moura
parent 5654d8465d
commit 2cb333a260
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/ElabRules.lean
View file

@ -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)