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