Documentation

Lean.Elab.PreDefinition.Basic

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

Instances For

    Applies Lean.instantiateMVars to the types of values of each predefinition.

    Equations
      Instances For

        Applies Lean.Elab.Term.levelMVarToParam to the types of each predefinition.

        Equations
          Instances For
            def Lean.Elab.fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) :
            Equations
              Instances For
                Equations
                  Instances For
                    Equations
                      Instances For

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

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

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

                                    Equations
                                      Instances For
                                        def Lean.Elab.ensureNoRecFn (recFnNames : Array Name) (e : Expr) :
                                        Equations
                                          Instances For

                                            Checks that all codomains have the same level, throws an error otherwise.

                                            Equations
                                              Instances For