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

fix: ppGoal bug

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-08 18:39:05 -08:00
parent b619b3ae7e
commit 62230defc7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Util/PPGoal.lean
View file

@ -21,7 +21,7 @@ match mctx.findDecl? mvarId with
match ids, type? with
| [], _ => fmt
| _, none => fmt
| _, some type => fmt ++ (Format.joinSep ids " " ++ " :" ++ Format.nest indent (Format.line ++ pp type)).group;
| _, 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;