Documentation of set-goal-arguments #914
Description
Line 49 in 997aa9b
Would it be possible to add documentation here explaining why this function takes two goal arguments?
Additionally, when a function takes a sealed-goal as argument, we might expect that the sealed-goal is required to have all its proof variables bound by nablas. But this function is called in some situations with the second argument as seal (goal ...), which means it's not always required to pass a self-contained goal. What should be the clue that the programmer is allowed to pass a self-contained goal to the function, as opposed to one which is just bound with seal but relies on metavariables with the context? Does solve have to return a fully self-contained goal or can it return goals with the proof variables in the context?