Documentation

Lean.Meta.GetUnfoldableConst

Equations
    Instances For

      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
        Instances For

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

          Equations
            Instances For