Documentation

Lean.Meta.Tactic.Clear

Erase the given free variable from the goal mvarId.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Try to erase the given free variable from the goal mvarId. It is no-op if the free variable cannot be erased due to forward dependencies.

    Equations
    Instances For

      Try to erase the given free variables from the goal mvarId.

      Equations
      Instances For