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.

Instances For

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

    Instances For