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

fix: extra line

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-27 09:11:04 -07:00
parent ed976027fe
commit 4495c13e6c
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Util/PPGoal.lean
View file

@ -17,11 +17,14 @@ match mctx.findDecl? mvarId with
let instMVars (e : Expr) : Expr := (mctx.instantiateMVars e).1;
let addLine (fmt : Format) : Format := if fmt.isNil then fmt else fmt ++ Format.line;
let pushPending (ids : List Name) (type? : Option Expr) (fmt : Format) : Format :=
let fmt := addLine fmt;
match ids, type? with
| [], _ => fmt
| _, none => fmt
| _, some type => fmt ++ (Format.joinSep ids.reverse " " ++ " :" ++ Format.nest indent (Format.line ++ pp type)).group;
if ids.isEmpty then
fmt
else
let fmt := addLine fmt;
match ids, type? with
| [], _ => fmt
| _, none => fmt
| _, some type => fmt ++ (Format.joinSep ids.reverse " " ++ " :" ++ Format.nest indent (Format.line ++ pp type)).group;
let (varNames, type?, fmt) := mvarDecl.lctx.foldl
(fun (acc : List Name × Option Expr × Format) (localDecl : LocalDecl) =>
let (varNames, prevType?, fmt) := acc;