Zulip Chat Archive

Stream: general

Topic: refl v rfl

view this post on Zulip Kevin Buzzard (Nov 26 2018 at 17:39):

I've always had it in the back of my mind that refl was slightly more general than rfl, because the tactic works with anything tagged @[refl]. But I've been trying to write a blog post about equality and I ran into this -- rfl working but refl not working.

example : set_of (λ x, x = 3) 3 := rfl

example : set_of (λ x, x = 3) 3 := by refl -- fails

What's happening there? For some reason refl is deciding not to unfold set_of, but it is not marked irreducible. There's something I'm not understanding correctly.

view this post on Zulip Chris Hughes (Nov 26 2018 at 17:43):

My guess is that it doesn't know that the relation in question is equality

Last updated: May 17 2021 at 22:15 UTC