Try to clear the given fvars from the local context. Returns the new goal and
the hypotheses that were cleared. Unlike Lean.MVarId.tryClearMany
, this
function does not require the hyps
to be given in the order in which they
appear in the local context.
Equations
- One or more equations did not get rendered due to their size.