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

Equations

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

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

Look up a constant name, returning the ConstantInfo if it 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 : Lake.Name) : Lean.MetaM (Option Lean.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.