From 0960cd0a14d944696559991b94d013276737e7ff Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sun, 18 Dec 2022 18:54:41 -0500 Subject: [PATCH] fix: term goal prefix --- src/Lean/Widget/InteractiveGoal.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean index 1e4f0dbf39..3492b03975 100644 --- a/src/Lean/Widget/InteractiveGoal.lean +++ b/src/Lean/Widget/InteractiveGoal.lean @@ -49,7 +49,7 @@ structure InteractiveGoalCore where structure InteractiveGoal extends InteractiveGoalCore where /-- The name `foo` in `case foo`, if any. -/ userName? : Option String - /-- The symbol to display before the target type. Usually `⊢` but `conv` goals use `∣` + /-- The symbol to display before the target type. Usually `⊢ ` but `conv` goals use `∣ ` and it could be extended. -/ goalPrefix : String /-- Identifies the goal (ie with the unique name of the MVar that it is a goal for.) -/ @@ -100,7 +100,7 @@ def InteractiveGoal.pretty (g : InteractiveGoal) : Format := g.toInteractiveGoalCore.pretty g.userName? g.goalPrefix def InteractiveTermGoal.pretty (g : InteractiveTermGoal) : Format := - g.toInteractiveGoalCore.pretty none "" + g.toInteractiveGoalCore.pretty none "⊢ " structure InteractiveGoals where goals : Array InteractiveGoal