Pierre Jouvelot (Apr 07 2022 at 12:49): Pierre Jouvelot (Apr 07 2022 at 12:49):Is there a particular reason why there is no \min in bigop.v or order.v (just a reserved notation)?
Emilio Jesús Gallego Arias (Apr 07 2022 at 12:49):I guess it is hard to pick the neutral element?
Pierre Jouvelot (Apr 07 2022 at 12:50):Not for nat.
Emilio Jesús Gallego Arias (Apr 07 2022 at 12:50):For nat there is no neutral element, right?
Emilio Jesús Gallego Arias (Apr 07 2022 at 12:51):what would it be?
Pierre Jouvelot (Apr 07 2022 at 12:52):Indeed. There would be an absorbing one. Still, \min could be useful for non-empty sets/lists.
Emilio Jesús Gallego Arias (Apr 07 2022 at 13:11):Yes I guess that's why the notation is reserved, so users can instantiate it if they have a bound
Pierre Jouvelot (Apr 07 2022 at 13:13):I see. Thanks.
Emilio Jesús Gallego Arias (Apr 07 2022 at 13:13):For order.v tho, it should be avaiable when the lattice has top
Emilio Jesús Gallego Arias (Apr 07 2022 at 13:14):If it is not, I guess that's a todo
Last updated: Apr 16 2024 at 11:01 UTC