refl v rfl

Stream: general

[Kevin Buzzard]

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.

[Chris Hughes]

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