Equiv.rfl

Stream: mathlib4

[Kevin Buzzard]

I just noticed that despite refl becoming rfl in Lean 4, we still have Equiv.refl in mathlib. Should it be changed to Equiv.rfl? Again this is coming from my preparing my course and thinking "is this confusing for the students?"

[Yaël Dillies]

We should if and only if we make the argument implicit.

[Kevin Buzzard]

Oh, that's what the distinction means now?

[Johan Commelin]

Also in Lean 3, viz le_refl x vs le_rfl.

[Kyle Miller]

docs#Eq.refl has an explicit argument, docs#rfl has an implicit argument. Similarly, docs#HEq.refl and docs#HEq.rfl

[Kevin Buzzard]

If this is the convention, I think it's a great one (because it's easy to explain)

[Mario Carneiro]

yes, this has always been the case (for theorem names)

[Mario Carneiro]

the tactic is special, but given that it doesn't take an argument the rfl name makes sense

[Yaël Dillies]

<insert always has been meme>