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

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.

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.