Zulip Chat Archive

Stream: new members

Topic: Unfold Notation


view this post on Zulip Marcus Rossel (Jan 15 2021 at 16:23):

Say I have the following:

structure some_type := (x : int) (y : int)

instance equiv : has_equiv some_type := λ l r, l.x = r.x

lemma eq_imp_equiv {s s' : some_type} : s = s'  s  s' :=
begin
  -- ⊢ s = s' → s ≈ s'
end

How do I unfold the in the goal?
Thanks :blush:

view this post on Zulip Alex J. Best (Jan 15 2021 at 16:59):

simp only [(≈)], is the way I usually unfold notation

view this post on Zulip Alex J. Best (Jan 15 2021 at 17:01):

However, much of the time this isn't necessary to prove the theorem, just to see what you're trying to prove!


Last updated: May 13 2021 at 18:26 UTC