This is the topic to ask questions on the talk "A hierarchy of ordered types in Mathematical Components".

Bump.

let's say I want to use the hierarchy to prove correctness of some algorithms on lattices from the literature. Do you feel the library is ready for this right now, or are there any obvious pieces missing?

Karl Palmskog said:

let's say I want to use the hierarchy to prove correctness of some algorithms on lattices from the literature. Do you feel the library is ready for this right now, or are there any obvious pieces missing?

Let me repeat (and rephrase) my answer: in most settings, the released version of order.v is ready for practical uses. But if you use duals heavily, there might be some pitfalls as observed in Coq-Polyhedra. Also, there is no interface for semilattices for now.

Last updated: Dec 07 2023 at 06:38 UTC