doc-next-gen

Init.Ext

Module docstring

{}

Lean.Parser.Attr.ext definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
syntax (name := ext) "ext" (ppSpace extIff)? (ppSpace extFlat)? (ppSpace prio)? : attr
Extensionality Attribute
Informal description
The `@[ext]` attribute registers an extensionality theorem for use with the `ext` tactic. When applied to a theorem, it generates an `ext_iff` theorem (unless disabled) and registers the original theorem for the `ext` tactic. When applied to a structure, it generates both `.ext` and `.ext_iff` theorems and registers the `.ext` theorem. Optional arguments include a priority value (default 1000), a flag to disable `ext_iff` generation, and a flag to control flattening of parent fields in structure extensionality theorems.
Lean.Elab.Tactic.Ext.ext definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
syntax (name := ext) "ext" (colGt ppSpace rintroPat)* (" : " num)? : tactic
Extensionality Tactic
Informal description
The `ext` tactic applies extensionality lemmas registered with the `@[ext]` attribute. It can be used in several ways: - `ext pat*` applies extensionality theorems as much as possible, using the patterns `pat*` to introduce variables via `rintro`. - Without patterns, `ext` applies extensionality lemmas as much as possible, introducing anonymous hypotheses when needed. - `ext pat* : n` applies extensionality theorems only up to depth `n`. The variant `ext1 pat*` applies only a single extensionality theorem. Unused patterns generate warnings, and mismatched patterns typically result in anonymous hypotheses.
Lean.Elab.Tactic.Ext.tacticExt1___ definition
: Lean.ParserDescr✝
Full source 
macromacro "ext1" xs:(colGt ppSpace rintroPat)* : tactic =>
  if xs.isEmpty then `(tactic| apply_ext_theorem <;> intros)
  else `(tactic| apply_ext_theorem <;> rintro $xs*)
Single-step extensionality tactic
Informal description
The tactic `ext1` applies a single extensionality theorem to the current goal, followed by introducing variables either anonymously (if no patterns are provided) or according to the given patterns (processed using `rintro`). This is in contrast to `ext` which recursively applies as many extensionality theorems as possible.
PUnit.ext theorem
(x y : PUnit) : x = y
Full source 
@[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
All Elements of `PUnit` Are Equal
Informal description
For any two elements $x$ and $y$ of the type `PUnit`, we have $x = y$.
Unit.ext theorem
(x y : Unit) : x = y
Full source 
protected theorem Unit.ext (x y : Unit) : x = y := rfl
All Elements of Unit Type are Equal
Informal description
For any two elements $x$ and $y$ of the type `Unit`, we have $x = y$.
Thunk.ext theorem
: {a b : Thunk α} → a.get = b.get → a = b
Full source 
@[ext] protected theorem Thunk.ext : {a b : Thunk α} → a.get = b.get → a = b
  | {..}, {..}, heq => congrArg _ <| funext fun _ => heq
Extensionality of Thunks: $a.\text{get} = b.\text{get} \to a = b$
Informal description
For any two thunks `a` and `b` of type `Thunk α`, if the values obtained by evaluating `a.get` and `b.get` are equal, then the thunks `a` and `b` themselves are equal.