Documentation

Init.Ext

The flag (iff := false) prevents ext from generating an ext_iff lemma.

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

    The flag (flat := false) causes ext to not flatten parents' fields when generating an ext lemma.

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

      Registers an extensionality theorem.

      • When @[ext] is applied to a theorem, the theorem is registered for the ext tactic, and it generates an "ext_iff" theorem. The name of the theorem is from adding the suffix _iff to the theorem name.

      • When @[ext] is applied to a structure, it generates an .ext theorem and applies the @[ext] attribute to it. The result is an .ext and an .ext_iff theorem with the .ext theorem registered for the ext tactic.

      • An optional natural number argument, e.g. @[ext 9000], specifies a priority for the ext lemma. Higher-priority lemmas are chosen first, and the default is 1000.

      • The flag @[ext (iff := false)] disables generating an ext_iff theorem.

      • The flag @[ext (flat := false)] causes generated structure extensionality theorems to show inherited fields based on their representation, rather than flattening the parents' fields into the lemma's equality hypotheses.

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

        Applies extensionality lemmas that are registered with the @[ext] attribute.

        • ext pat* applies extensionality theorems as much as possible, using the patterns pat* to introduce the variables in extensionality theorems using rintro. For example, the patterns are used to name the variables introduced by lemmas such as funext.
        • Without patterns,ext applies extensionality lemmas as much as possible but introduces anonymous hypotheses whenever needed.
        • ext pat* : n applies ext theorems only up to depth n.

        The ext1 pat* tactic is like ext pat* except that it only applies a single extensionality theorem.

        Unused patterns will generate warning. Patterns that don't match the variables will typically result in the introduction of anonymous hypotheses.

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

          Apply a single extensionality theorem to the current goal.

          Equations
          Instances For

            ext1 pat* is like ext pat* except that it only applies a single extensionality theorem rather than recursively applying as many extensionality theorems as possible.

            The pat* patterns are processed using the rintro tactic. If no patterns are supplied, then variables are introduced anonymously using the intros tactic.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem Sigma.ext {α : Type u} {β : αType v} {x : Sigma β} {y : Sigma β} (fst : x.fst = y.fst) (snd : HEq x.snd y.snd) :
              x = y
              theorem Prod.ext_iff {α : Type u} {β : Type v} {x : α × β} {y : α × β} :
              x = y x.fst = y.fst x.snd = y.snd
              theorem Sigma.ext_iff {α : Type u} {β : αType v} {x : Sigma β} {y : Sigma β} :
              x = y x.fst = y.fst HEq x.snd y.snd
              theorem Prod.ext {α : Type u} {β : Type v} {x : α × β} {y : α × β} (fst : x.fst = y.fst) (snd : x.snd = y.snd) :
              x = y
              theorem PSigma.ext {α : Sort u} {β : αSort v} {x : PSigma β} {y : PSigma β} (fst : x.fst = y.fst) (snd : HEq x.snd y.snd) :
              x = y
              theorem PProd.ext_iff {α : Sort u} {β : Sort v} {x : α ×' β} {y : α ×' β} :
              x = y x.fst = y.fst x.snd = y.snd
              theorem PProd.ext {α : Sort u} {β : Sort v} {x : α ×' β} {y : α ×' β} (fst : x.fst = y.fst) (snd : x.snd = y.snd) :
              x = y
              theorem PSigma.ext_iff {α : Sort u} {β : αSort v} {x : PSigma β} {y : PSigma β} :
              x = y x.fst = y.fst HEq x.snd y.snd
              theorem Subtype.eq_iff {α : Type u} {p : αProp} {a1 : { x : α // p x }} {a2 : { x : α // p x }} :
              a1 = a2 a1.val = a2.val
              theorem Array.ext_iff {α : Type u} {a : Array α} {b : Array α} :
              a = b a.size = b.size ∀ (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b.size), a[i] = b[i]
              theorem funext_iff {α : Sort u} {β : αSort v} {f : (x : α) → β x} {g : (x : α) → β x} :
              f = g ∀ (x : α), f x = g x
              theorem propext_iff {a : Prop} {b : Prop} :
              a = b (a b)
              theorem PUnit.ext_iff {x : PUnit} {y : PUnit} :
              x = y True
              theorem PUnit.ext (x : PUnit) (y : PUnit) :
              x = y
              theorem Unit.ext (x : Unit) (y : Unit) :
              x = y
              theorem Thunk.ext_iff {α : Type u_1} {a : Thunk α} {b : Thunk α} :
              a = b a.get = b.get
              theorem Thunk.ext {α : Type u_1} {a : Thunk α} {b : Thunk α} :
              a.get = b.geta = b