Documentation

Lean.Elab.PreDefinition.Structural.FindRecArg

Equations
    Instances For
      Equations
        Instances For
          Equations
            Instances For
              def Lean.Elab.Structural.getRecArgInfo (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array Expr) (i : Nat) :

              Assemble the RecArgInfo for the ith parameter in the parameter list xs. This performs various sanity checks on the parameter (is it even of inductive type etc).

              Equations
                Instances For
                  def Lean.Elab.Structural.getRecArgInfos (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array Expr) (value : Expr) (termMeasure? : Option TerminationMeasure) :

                  Collects the RecArgInfos for one function, and returns a report for why the others were not considered.

                  The xs are the fixed parameters, value the body with the fixed prefix instantiated.

                  Takes the optional user annotation into account (termMeasure?). If this is given and the measure is unsuitable, throw an error.

                  Equations
                    Instances For

                      Reorders the RecArgInfos of one function to put arguments that are indices of other arguments last. See issue #837 for an example where we can show termination using the index of an inductive family, but we don't get the desired definitional equalities.

                      Equations
                        Instances For

                          Given the RecArgInfos of all the recursive functions, find the inductive groups to consider.

                          Equations
                            Instances For

                              Filters the recArgInfos by those that describe an argument that's part of the recursive inductive group group.

                              Because of nested inductives this function has the ability to change the recArgInfo. Consider

                              inductive Tree where | node : List Tree → Tree
                              

                              then when we look for arguments whose type is part of the group Tree, we want to also consider the argument of type List Tree, even though that argument’s RecArgInfo refers to initially to List.

                              Equations
                                Instances For
                                  Equations
                                    Instances For
                                      @[irreducible]
                                      def Lean.Elab.Structural.allCombinations.go {α : Type u_1} (xss : Array (Array α)) (i : Nat) (acc : Array α) :
                                      Equations
                                        Instances For
                                          def Lean.Elab.Structural.tryAllArgs {α : Type} (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs values : Array Expr) (termMeasure?s : Array (Option TerminationMeasure)) (k : Array RecArgInfoM α) :
                                          M α
                                          Equations
                                            Instances For