should le_refl be @[refl]

Stream: general

[Johan Commelin]

I think that @[refl] is meant as a tag for lemmas that prove that a relation is reflexive. Should le_refl be tagged with @[refl]?

[Kenny Lau]

that's a heavy yes from me

[Mario Carneiro]

it is

[Kenny Lau]

then why doesn't refl work?

[Mario Carneiro]

apply bug probably

[Kevin Buzzard]

apply bug probably

I want to make a badge which says that. Out of context that's a great sentence.