mathlib

mathlib copied to clipboard

Toy example:

import tactic.ext

@[ext] structure foo (α : Type*) :=
(a : α)
(b : unit)

#check @foo.ext

The generated lemma has type foo.ext : ∀ {α : Type u_1} (x y : foo α), x.a = y.a → x.b = y.b → x = y, in which the hypothesis x.b = y.b is always satisfied; instead the lemma should only take the x.a = y.a hypothesis.

In this example, the extra hypothesis doesn't matter so much, because unit also has an extensionality lemma which will be applied by the ext tactic. But you might want to apply the foo.ext lemma by hand, and there are other subsingleton types without ext lemmas (e.g. trunc β).