Stream: Coq workshop 2020

Topic: [M2] A hierarchy of ordered types in Mathematical Components


view this post on Zulip 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".

view this post on Zulip Kazuhiko Sakaguchi (Jul 06 2020 at 08:19):

Bump.

view this post on Zulip 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?

view this post on Zulip 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: Feb 06 2023 at 06:29 UTC