ext
on structures should use subsingleton
instances to avoid unnecessary hypotheses
#4336
Labels
t-meta
Tactics, attributes or user commands
Toy example:
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 hypothesisx.b = y.b
is always satisfied; instead the lemma should only take thex.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 theext
tactic. But you might want to apply thefoo.ext
lemma by hand, and there are other subsingleton types withoutext
lemmas (e.g.trunc β
).The text was updated successfully, but these errors were encountered: