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

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) : Lean.MetaM Unit

Equations

• Lean.Meta.refl mvarId = Lean.MVarId.refl mvarId

def Lean.MVarId.applyRefl (mvarId : Lean.MVarId) (msg : optParam Lean.MessageData (Function.comp Lean.MessageData.ofFormat Std.format "refl failed")) : Lean.MetaM Unit

Equations

• Lean.MVarId.applyRefl mvarId msg = tryCatch (Lean.MVarId.refl mvarId) fun x => Lean.throwError msg

def Lean.MVarId.heqOfEq (mvarId : Lean.MVarId) : Lean.MetaM Lean.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 : Lean.MVarId) : Lean.MetaM Lean.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 : Lean.MVarId) : Lean.MetaM Unit

Close given goal using HEq.refl.

Equations

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