Documentation

Lean.Meta.IndPredBelow

The context used in the creation of the below scheme for inductive predicates.

Instances For

    Collection of variables used to keep track of the positions of binders in the construction of below motives and constructors.

    Instances For
      Equations
      • One or more equations did not get rendered due to their size.

      Collection of variables used to keep track of the local context used in the brecOn proof.

      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For

                                                            Given a constructor name, find the indices of the corresponding below version thereof.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              partial def Lean.Meta.IndPredBelow.getBelowIndices.loop (xs : Array Lean.Expr) (rest : Lean.Expr) (belowIndices : Array Nat) (xIdx : Nat) (yIdx : Nat) :

                                                              This function adds an additional below discriminant to a matcher application. It is used for modifying the patterns, such that the structural recursion can use the new below predicate instead of the original one and thus be used prove structural recursion.

                                                              It takes as parameters:

                                                              • matcherApp: a matcher application
                                                              • belowMotive: the motive, that the below type should carry
                                                              • below: an expression from the local context that is the below version of a predicate and can be used for structural recursion
                                                              • idx: the index of the original predicate discriminant.

                                                              It returns:

                                                              • A matcher application as an expression
                                                              • A side-effect for adding the matcher to the environment
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For

                                                                  this function changes the type of the pattern from the original type to the below version thereof. Most of the cases don't apply. In order to change the type and the pattern to be type correct, we don't simply recursively change all occurrences, but rather, we recursively change occurrences of the constructor. As such there are only a few cases:

                                                                  • the pattern is a constructor from the original type. Here we need to:
                                                                    • replace the constructor
                                                                    • copy original recursive patterns and convert them to below and reintroduce them in the correct position
                                                                    • turn original recursive patterns inaccessible
                                                                    • introduce free variables as needed.
                                                                  • it is an as pattern. Here the constructor could be hidden inside of it.
                                                                  • it is a variable. Here you we need to introduce a fresh variable of a different type.
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For

                                                                      Generates the auxiliary lemmas below and brecOn for a recursive inductive predicate. The current generator doesn't support nested predicates, but pattern-matching on them still works thanks to well-founded recursion.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For