doc: Correct comment about parent filling expr
This commit is contained in:
parent
25f3a2f19d
commit
40d61fecc5
|
@ -241,7 +241,7 @@ structure GoalPrint where
|
||||||
structure GoalPrintResult where
|
structure GoalPrintResult where
|
||||||
-- The root expression
|
-- The root expression
|
||||||
root?: Option Expression := .none
|
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
|
parent?: Option Expression := .none
|
||||||
deriving Lean.ToJson
|
deriving Lean.ToJson
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue