Documentation

Std.Lean.Meta.Clear

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.
Instances For