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.

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

Alternative can-unfold predicate used inside whnfMatcher. See module comment above unfoldNestedDIte in Lean.Meta.WHNF.

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

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.

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

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