Zulip Chat Archive
Stream: general
Topic: should le_refl be @[refl]
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]?
Kenny Lau (Jul 05 2019 at 14:22):
that's a heavy yes from me
Mario Carneiro (Jul 05 2019 at 14:31):
it is
Kenny Lau (Jul 05 2019 at 14:33):
then why doesn't refl work?
Mario Carneiro (Jul 05 2019 at 14:34):
apply bug probably
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: Dec 20 2023 at 11:08 UTC