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

doc: fix docstring for InteractiveGoal

Browse source
This commit is contained in:
E.W.Ayers 2022-06-13 17:20:47 -04:00 • committed by Leonardo de Moura
parent 2edf02544e
commit 13e286f545
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/Lean/Widget/InteractiveGoal.lean
View file

@ -30,7 +30,7 @@ structure InteractiveGoal where
goalPrefix : String
/-- Identifies the goal (ie with the unique
name of the MVar that it is a goal for.)
[todo] what should the key be for a term goal?-/
This is none when we are showing a term goal. -/
mvarId? : Option MVarId := none
deriving Inhabited, RpcEncoding