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

fix: term goal prefix

Browse source
This commit is contained in:
Wojciech Nawrocki 2022-12-18 18:54:41 -05:00 • committed by Gabriel Ebner
parent f5531c2a11
commit 0960cd0a14
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Widget/InteractiveGoal.lean
View file

@ -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