# Documentation

Lean.Meta.Tactic.Refl

def Lean.MVarId.refl (mvarId : Lean.MVarId) :

Close given goal using Eq.refl.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.refl (mvarId : Lean.MVarId) :
Equations
def Lean.MVarId.applyRefl (mvarId : Lean.MVarId) (msg : optParam Lean.MessageData ((Lean.MessageData.ofFormat Std.format) "refl failed")) :
Equations

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.

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.

Close given goal using HEq.refl.

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