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.canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool

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

Equations

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

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

Equations

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

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.