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

feat: use if-then-else notation at Do.lean

Browse source 
Otherwise, the `if` in the `Do` notation will not benefit from the
improved elaborator.
This commit is contained in:
Leonardo de Moura 2021-09-30 22:34:36 -07:00
parent 9d9f41c27a
commit b99f1c698b
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Do.lean
View file

@ -991,10 +991,10 @@ def reassignToTerm (reassign : Syntax) (k : Syntax) : MacroM Syntax := withRef r
def mkIte (optIdent : Syntax) (cond : Syntax) (thenBranch : Syntax) (elseBranch : Syntax) : MacroM Syntax := do
if optIdent.isNone then
``(ite $cond $thenBranch $elseBranch)
``(if $cond then $thenBranch else $elseBranch)
else
let h := optIdent[0]
``(dite $cond (fun $h => $thenBranch) (fun $h => $elseBranch))
``(if $h:ident : $cond then $thenBranch else $elseBranch)
def mkJoinPoint (j : Name) (ps : Array (Name × Bool)) (body : Syntax) (k : Syntax) : M Syntax := withRef body <| withFreshMacroScope do
let pTypes ← ps.mapM fun ⟨id, useTypeOf⟩ => do if useTypeOf then `(typeOf% $(← mkIdentFromRef id)) else `(_)