From 51904224db05893117dbf320556cb26064818582 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Jan 2020 15:29:23 -0800 Subject: [PATCH] feat: display goal tag --- src/Init/Lean/Util/PPGoal.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Init/Lean/Util/PPGoal.lean b/src/Init/Lean/Util/PPGoal.lean index b5f2909384..bd1d058966 100644 --- a/src/Init/Lean/Util/PPGoal.lean +++ b/src/Init/Lean/Util/PPGoal.lean @@ -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