Documentation

Lean.Meta.Tactic.Refl

Close given goal using Eq.refl.

See Lean.MVarId.applyRfl for the variant that also consults @[refl] lemmas, and which backs the rfl tactic.

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

    Try to apply heq_of_eq. If successful, then return new goal, otherwise return mvarId.

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

      Try to apply eq_of_heq. If successful, then return new goal, otherwise return mvarId.

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

        Close given goal using HEq.refl.

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