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

fix: checkWsBefore.formatter

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-06 17:11:50 +02:00
parent 064c9b2e0b
commit f0dad079ad
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -382,7 +382,9 @@ def toggleInsideQuot.formatter (p : Formatter) : Formatter :=
p
@[combinatorFormatter checkWsBefore] def checkWsBefore.formatter : Formatter := do
pushLine
st ← get;
when (st.leadWord != "") $
pushLine
@[combinatorFormatter checkPrec] def checkPrec.formatter : Formatter := pure ()
@[combinatorFormatter checkStackTop] def checkStackTop.formatter : Formatter := pure ()

2
tests/lean/precissues.lean.expected.out
View file

@ -10,7 +10,7 @@ precissues.lean:17:10: error: expected command, but found term; this error may b
1 : Nat
id ((fun (this : True) => this) True.intro) : True
0 = (fun (this : Nat) => this) 1 : Prop
0 = let x : Nat := 0;
0 = let x : Nat := 0;
x : Prop
p ↔ ¬q : Prop
True = ¬False : Prop