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

chore: runTermElabM refactor

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-07 07:30:29 -07:00
parent a7e0e5b50a
commit 1c5ec65260
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/DSL/Meta.lean
View file

@ -53,7 +53,7 @@ scoped syntax (name := metaIf)
"meta " "if " term " then " cmdDo (" else " cmdDo)? : command
elab_rules : command | `(meta if $c then $t $[else $e?]?) => do
if (← withRef c <| runTermElabM none <| fun _ => evalTerm Bool c) then
if (← withRef c <| runTermElabM fun _ => evalTerm Bool c) then
let cmd := mkNullNode (expandCmdDo t)
withMacroExpansion (← getRef) cmd <| elabCommand cmd
else if let some e := e? then