Documentation

Lean.Meta.Tactic.Ext

Environment extension for ext theorems #

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

  • declName : 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
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      Instances For
        Equations
        Instances For

          The state of the ext extension environment

          Instances For

            The environment extension to track @[ext] theorems.

            @[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

                Returns true if d contains theorem with name declName.

                Equations
                Instances For

                  Returns true if declName is tagged with [ext] attribute.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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