ext_iff not getting defined

Stream: new members

[ROCKY KAMEN-RUBIO]

I've been trying some variations of Kevin's livestream today, I'm confused why ext_iff isn't getting defined for some of my structures.

import tactic
import data.nat.basic

structure silly (n : ℕ) :=
(k : ℕ)
(h : k = n)
(l : ℕ)

def x : silly 1 := silly.mk 1 (by refl) 2
def y : silly 1 := silly.mk 1 (by refl) 3
example : x ≠ y :=
begin
  unfold x,
  unfold y,
  intro h,
  --rw silly.ext_iff at h,
  sorry,
end

structure silly2 :=
(k : ℕ)

def x' : silly2 := silly2.mk 1
def y' : silly2 := silly2.mk 2
example : x' ≠ y' :=
begin
  intro h,
  --rw silly2.ext_iff at h,
  sorry
end

[Alex J. Best]

ext_iff  is generated by adding the @[ext] attribute to your structures I believe

[ROCKY KAMEN-RUBIO]

Alex J. Best said:

ext_iff  is generated by adding the @[ext] attribute to your structures I believe

Thank you! Just seeing now that I missed that part of the video when I went back to this section. Thanks!