diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 7413cdb6b7..6f565cd2ed 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -375,7 +375,7 @@ p @[combinatorFormatter checkWsBefore] def checkWsBefore.formatter : Formatter := do modify fun st => { st with leadWord := "" }; -push " " +pushLine @[combinatorFormatter checkPrec] def checkPrec.formatter : Formatter := pure () @[combinatorFormatter checkStackTop] def checkStackTop.formatter : Formatter := pure () diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out index 89428e4839..d0b789e831 100644 --- a/tests/lean/PPRoundtrip.lean.expected.out +++ b/tests/lean/PPRoundtrip.lean.expected.out @@ -20,7 +20,9 @@ fun (b : Bool) => a fun {a b : Nat} => a -typeAs ({α : Type} → α → α) fun +typeAs + ({α : Type} → α → α) + fun {α : Type} (a : α) => a @@ -52,6 +54,6 @@ Type → Type → Type (1, 2, 3) (1, 2).fst 1 < 2 || true -id (fun - (a : Nat) => - a) 0 +id + (fun (a : Nat) => a) + 0