Documentation

Lean.Elab.Tactic.Ext

Implementation of the @[ext] attribute #

Meta code for creating ext theorems #

Constructs the hypotheses for the structure extensionality theorem that states that two structures are equal if their fields are equal.

Calls the continuation k with the list of parameters to the structure, two structure variables x and y, and a list of pairs (field, ty) where each ty is of the form x.field = y.field or HEq x.field y.field.

If flat parses to true, any fields inherited from parent structures are treated as fields of the given structure type. If it is false, then the behind-the-scenes encoding of inherited fields is visible in the extensionality lemma.

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

    Creates the type of the extensionality theorem for the given structure, returning ∀ {x y : Struct}, x.1 = y.1 → x.2 = y.2 → x = y, for example.

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

      Derives the type of the iff form of an ext theorem.

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

        Ensures that the given structure has an ext theorem, without validating any pre-existing theorems. Returns the name of the ext theorem.

        See Lean.Elab.Tactic.Ext.withExtHyps for an explanation of the flat argument.

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

          Given an 'ext' theorem, ensures that there is an iff version of the theorem (if possible), without validating any pre-existing theorems. Returns the name of the 'ext_iff' theorem.

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

            Attribute #

            Information about an extensionality theorem, stored in the environment extension.

            • declName : Lake.Name

              Declaration name of the extensionality theorem.

            • priority : Nat

              Priority of the extensionality theorem.

            • Key in the discrimination tree, for the type in which the extensionality theorem holds.

            Instances For
              Equations

              The state of the ext extension environment

              Instances For

                Discrimation tree settings for the ext extension.

                Equations
                Instances For
                  @[inline]

                  Gets the list of @[ext] theorems corresponding to the key ty, ordered from high priority to low.

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

                    Erases a name marked ext by adding it to the state's erased field and removing it from the state's list of Entrys.

                    This is triggered by attribute [-ext] name.

                    Equations
                    Instances For

                      Erases a name marked as a ext attribute. Check that it does in fact have the ext attribute by making sure it names a ExtTheorem found somewhere in the state's tree, and is not erased.

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

                        Implementation of ext tactic #

                        Apply a single extensionality theorem to goal.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def Lean.Elab.Tactic.Ext.tryIntros {m : TypeType u_1} [Monad m] [MonadLiftT Lean.Elab.TermElabM m] (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (k : Lean.MVarIdList (Lean.TSyntax `rcasesPat)m Nat) :
                          m Nat

                          Postprocessor for withExt which runs rintro with the given patterns when the target is a pi type.

                          Equations
                          Instances For
                            def Lean.Elab.Tactic.Ext.withExt1 {m : TypeType u_1} [Monad m] [MonadLiftT Lean.Elab.TermElabM m] (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (k : Lean.MVarIdList (Lean.TSyntax `rcasesPat)m Nat) :
                            m Nat

                            Applies a single extensionality theorem, using pats to introduce variables in the result. Runs continuation k on each subgoal.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def Lean.Elab.Tactic.Ext.withExtN {m : TypeType u_1} [Monad m] [MonadLiftT Lean.Elab.TermElabM m] [MonadExcept Lean.Exception m] (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (k : Lean.MVarIdList (Lean.TSyntax `rcasesPat)m Nat) (depth : optParam Nat 1000000) (failIfUnchanged : optParam Bool true) :
                              m Nat

                              Applies extensionality theorems recursively, using pats to introduce variables in the result. Runs continuation k on each subgoal.

                              Equations
                              Instances For
                                def Lean.Elab.Tactic.Ext.extCore (g : Lean.MVarId) (pats : List (Lean.TSyntax `rcasesPat)) (depth : optParam Nat 1000000) (failIfUnchanged : optParam Bool true) :

                                Apply extensionality theorems as much as possible, using pats to introduce the variables in extensionality theorems like funext. Returns a list of subgoals.

                                This is built on top of withExtN, running in TermElabM to build the list of new subgoals. (And, for each goal, the patterns consumed.)

                                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