[Isarmathlib-devel] Partial orders as locales?

[Victor Porton]

Should we re-implement partial orders and strict partial orders as locales?

The arguments pro:

1. Relation of partial orders and strict partial orders could be adequately 
described as sublocales (I'm not 100% sure that here will be not a bad infinite 
loop, please correct me about the loop.)

2. Such orders would naturally fit into ongoing lattice and complete_lattice 
locales.

I also suggest to add "indefinite" value which could (for example) mean a 
non-existing supremum. (We can define "indefinite" to be equal with the base 
set, because a set cannot be its own member.)

I consider to take time to make this formalization work for IsarMathLib. So 
treat me seriously.

-- 
Victor Porton - http://portonvictor.org