Zulip Chat Archive

Stream: general

Topic: should le_refl be @[refl]


view this post on Zulip Johan Commelin (Jul 05 2019 at 14:18):

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]?

view this post on Zulip Kenny Lau (Jul 05 2019 at 14:22):

that's a heavy yes from me

view this post on Zulip Mario Carneiro (Jul 05 2019 at 14:31):

it is

view this post on Zulip Kenny Lau (Jul 05 2019 at 14:33):

then why doesn't refl work?

view this post on Zulip Mario Carneiro (Jul 05 2019 at 14:34):

apply bug probably

view this post on Zulip Kevin Buzzard (Jul 05 2019 at 14:35):

apply bug probably

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


Last updated: May 13 2021 at 19:20 UTC