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

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

      Equations
        Instances For

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

          Equations
            Instances For

              Close given goal using HEq.refl.

              Equations
                Instances For