Stream: math-comp users

Topic: 0.+1

view this post on Zulip Pierre-Yves Strub (Sep 17 2021 at 09:31):

Hey. I just got this in some goal: c 0.+1 (coq 8.13.0 & mathcomp 1.12.0). Seems pretty weird.

view this post on Zulip Pierre-Yves Strub (Sep 17 2021 at 09:32):

Hmmm. Got it. The 0 was from Order.

view this post on Zulip Florent Hivert (Sep 17 2021 at 09:38):

I really dislike the notations 0 and 1 from Order. I would strongly vote for bot and top or something similar. For example, I formalized the weak order on the symmetric group. The smallest element 0%O is the identity permutation 1%G. It was very confusing.

view this post on Zulip Pierre-Yves Strub (Sep 17 2021 at 09:39):

In any case, in the nat scope, 0%N should be preferred over 0%O.

Last updated: Oct 13 2024 at 01:02 UTC