Documentation

Lean.Elab.PreDefinition.Basic

A (potentially recursive) definition. The elaborator converts it into Kernel definitions using many different strategies.

Instances For

Auxiliary method for (temporarily) adding pre definition as an axiom

Instances For
    def Lean.Elab.addNonRec (preDef : Lean.Elab.PreDefinition) (applyAttrAfterCompilation : optParam Bool true) (all : optParam (List Lake.Name) [preDef.declName]) :
    Instances For

      Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module to produce better error messages.

      Instances For