def Lean.Meta.canUnfold (info : ConstantInfo) : MetaM Bool

Equations

• Lean.Meta.canUnfold info = do let ctx ← read let cfg ← Lean.Meta.getConfig match ctx.canUnfold? with | some f => liftM (f cfg info) | x => liftM (Lean.Meta.canUnfoldDefault✝ cfg info)

def Lean.Meta.getUnfoldableConst? (constName : Name) : MetaM (Option ConstantInfo)

Look up a constant name, returning the ConstantInfo if it is a def/theorem that should be unfolded at the current reducibility settings, or none otherwise.

This is part of the implementation of whnf. External users wanting to look up names should be using Lean.getConstInfo.

Equations

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

def Lean.Meta.getUnfoldableConstNoEx? (constName : Name) : MetaM (Option ConstantInfo)

As with getUnfoldableConst? but return none instead of failing if the constant is not found.

Equations

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