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

feat: display goal tag

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-18 15:29:23 -08:00
parent d41325681d
commit 51904224db
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -43,6 +43,9 @@ match mctx.findDecl? mvarId with
([], none, Format.nil);
let fmt := pushPending varNames type? fmt;
let fmt := addLine fmt;
fmt ++ "⊢" ++ " " ++ Format.nest indent (pp mvarDecl.type)
let fmt := fmt ++ "⊢" ++ " " ++ Format.nest indent (pp mvarDecl.type);
match mvarDecl.userName with
| Name.anonymous => fmt
| name => "case " ++ format name ++ Format.line ++ fmt
end Lean