def Lean.Meta.canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool

Implements the TransparencyMode hierarchy for unfolding decisions. See TransparencyMode and ReducibilityStatus for the design rationale.

Equations

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

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.