refl and rfl

Stream: new members

[Alex Zhang]

What is the difference between tactics refl and rfl?

[Kevin Buzzard]

Are you sure rfl is a tactic? What happens if you put it in a begin/end block?

[Alex Zhang]

No...I don't think rfl is a tactic now.

[Kevin Buzzard]

so rfl is a term, you can use it in term mode to prove x = x, e.g.

example : 2 = 2 := rfl

And refl is a tactic, so you can use it in tactic mode to prove x = x, e.g.

example : 2 = 2 :=
begin
  refl
end

[Mario Carneiro]

Speaking of which, perhaps we should rename refl tactic to rfl for consistency with lean 4? I don't think it's a very big deal but we may as well get in the habit

[Kevin Buzzard]

I think lean 4's rfl tactic only does eq.rfl so we might end up making a refl tactic anyway

[Mario Carneiro]

I'd rather just override the rfl tactic when the time comes