diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index fcc253f..84e0cc2 100644 --- 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