def Lean.Meta.tryURefl (mvarId : Lean.MVarId) : Lean.MetaM Bool

Try to close goal using rfl with smart unfolding turned off.

Equations

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

def Lean.Meta.getConstUnfoldEqnFor? (declName : Lake.Name) : Lean.MetaM (Option Lake.Name)

Returns the "const unfold" theorem (f.eq_unfold) for the given declaration. This is not extensible, and always builds on the unfold theorem (f.eq_def).

Equations

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