Documentation

Lean.Elab.PreDefinition.WF.PackMutual

This module contains roughly everything needed to turn mutual n-ary functions into a single unary function, as used by well-founded recursion.

Pass the first n arguments of e to the continuation, and apply the result to the remaining arguments. If e does not have enough arguments, it is eta-expanded as needed.

Unlike Meta.etaExpand does not use withDefault.

Equations
    Instances For
      def Lean.Elab.WF.packCalls (fixedParamPerms : FixedParamPerms) (argsPacker : Meta.ArgsPacker) (funNames : Array Name) (newF e : Expr) :

      Processes the expression and replaces calls to the preDefs with calls to f.

      Equations
        Instances For
          def Lean.Elab.WF.mutualName (fixedParamPerms : FixedParamPerms) (argsPacker : Meta.ArgsPacker) (preDefs : Array PreDefinition) :
          Equations
            Instances For

              Creates a single unary function from the given preDefs, using the machinery in the ArgPacker module.

              Equations
                Instances For
                  def Lean.Elab.WF.varyingVarNames (fixedParamPerms : FixedParamPerms) (preDefIdx : Nat) (preDef : PreDefinition) :

                  Collect the names of the varying variables (excluding the fixed parameters); this also determines the arity for the well-founded translations, and is turned into an ArgsPacker. We use the term to determine the arity, but take the name from the type, for better names in the

                  fun : (n : Nat) → Nat | 0 => 0 | n+1 => fun n
                  

                  idiom.

                  Equations
                    Instances For
                      def Lean.Elab.WF.preDefsFromUnaryNonRec (fixedParamPerms : FixedParamPerms) (argsPacker : Meta.ArgsPacker) (preDefs : Array PreDefinition) (unaryPreDefNonRec : PreDefinition) :
                      Equations
                        Instances For