fix: use group for if-then-else

src/Init/Notation.lean

@@ -137,12 +137,16 @@ infixr:100 " <$> " => Functor.map
 macro_rules | `($x <|> $y) => `(binop_lazy% HOrElse.hOrElse $x $y)
 macro_rules | `($x >> $y)  => `(binop_lazy% HAndThen.hAndThen $x $y)
 
-syntax (name := termDepIfThenElse) ppGroup(ppDedent("if " ident " : " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
+syntax (name := termDepIfThenElse)
+  ppRealGroup(ppRealFill(ppIndent("if " ident " : " term " then") ppSpace term)
+    ppDedent(ppSpace) ppRealFill("else " term)) : term
 
 macro_rules
   | `(if $h:ident : $c then $t:term else $e:term) => `(let_mvar% ?m := $c; wait_if_type_mvar% ?m; dite ?m (fun $h:ident => $t) (fun $h:ident => $e))
 
-syntax (name := termIfThenElse) ppGroup(ppDedent("if " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
+syntax (name := termIfThenElse)
+  ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace term)
+    ppDedent(ppSpace) ppRealFill("else " term)) : term
 
 macro_rules
   | `(if $c then $t:term else $e:term) => `(let_mvar% ?m := $c; wait_if_type_mvar% ?m; ite ?m $t $e)

tests/lean/ppite.lean.expected.out

@@ -3,10 +3,12 @@ fun xs =>
   List.forM xs fun x =>
     if (x == 0) = true then do
       IO.println "foo"
-      IO.println "zero" else
+      IO.println "zero"
+    else
       if (x % 2 == 0) = true then do
         IO.println x
-        IO.println "even" else do
+        IO.println "even"
+      else do
         IO.println x
         IO.println "odd"
 if true = true then 1 else 0 : Nat

tests/lean/wfrecUnusedLet.lean.expected.out

@@ -1,5 +1,6 @@
 def f : Nat → Nat :=
 WellFounded.fix f.proof_1 fun x a =>
-  if h : x = 0 then 1 else
+  if h : x = 0 then 1
+  else
     let y := 42;
     2 * a (x - 1) (_ : (measure id).1 (x - 1) x)