doc: Correct comment about parent filling expr

2024-01-30 16:37:35 -08:00 · 2024-01-30 16:37:35 -08:00 · 6d22841a27
parent 9a5ee49778
commit 6d22841a27
1 changed files with 1 additions and 1 deletions
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -241,7 +241,7 @@ structure GoalPrint where
 structure GoalPrintResult where
  -- The root expression
  root?: Option Expression := .none
-  -- How is this goal filled in relation to its children?
+  -- The filling expression of the parent goal
  parent?: Option Expression := .none
  deriving Lean.ToJson