Théo Zimmermann (Jun 24 2020 at 11:20): Théo Zimmermann (Jun 24 2020 at 11:20):This is the topic to ask questions on the talk "A hierarchy of ordered types in Mathematical Components".
Kazuhiko Sakaguchi (Jul 06 2020 at 08:19):Bump.
Karl Palmskog (Jul 06 2020 at 08:40):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?
Kazuhiko Sakaguchi (Jul 06 2020 at 09:13):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: Apr 16 2024 at 20:02 UTC