From 13e286f54580165d16592ccab4538d302d2ed32c Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Mon, 13 Jun 2022 17:20:47 -0400 Subject: [PATCH] doc: fix docstring for InteractiveGoal --- src/Lean/Widget/InteractiveGoal.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean index b69b3d2712..d94ace5f20 100644 --- a/src/Lean/Widget/InteractiveGoal.lean +++ b/src/Lean/Widget/InteractiveGoal.lean @@ -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