Documentation

Lean.Meta.Tactic.Assumption

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

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

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[deprecated Lean.MVarId.assumptionCore]
      Equations
      Instances For

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[deprecated Lean.MVarId.assumption]
          Equations
          Instances For