From b99f1c698b5d53019cabe54f03567c546ca9faab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Sep 2021 22:34:36 -0700 Subject: [PATCH] feat: use `if-then-else` notation at `Do.lean` Otherwise, the `if` in the `Do` notation will not benefit from the improved elaborator. --- src/Lean/Elab/Do.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 3aac240c53..0c3bef1cfb 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -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 `(_)