Documentation

Lean.Meta.Tactic.Assumption

Return a local declaration whose type is definitionally equal to type.

Equations
    Instances For

      Return true if managed to close goal mvarId using an assumption.

      Equations
        Instances For

          Close goal mvarId using an assumption. Throw error message if failed.

          Equations
            Instances For