def Lean.MVarId.refl (mvarId : MVarId) (check : Bool := true) : MetaM Unit

Close given goal using Eq.refl.

With (check := false), the elaborator does not check if the goal is actually a definitionaly equality.

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.

def Lean.MVarId.heqOfEq (mvarId : MVarId) : MetaM MVarId

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.

def Lean.MVarId.eqOfHEq (mvarId : MVarId) : MetaM MVarId

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.

def Lean.MVarId.hrefl (mvarId : MVarId) : MetaM Unit

Close given goal using HEq.refl.

Equations

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