Is there a particular reason why there is no
order.v (just a reserved notation)?
I guess it is hard to pick the neutral element?
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: Jan 29 2023 at 18:03 UTC