ekmett / ersatz

A monad for interfacing with external SAT solvers
Other
63 stars 15 forks source link

Add module for order theory-related properties #85

Open emeinhardt opened 8 months ago

emeinhardt commented 8 months ago

Per the title, adds a module full of properties related to order-theoretic structures for use with homogeneous binary relations; generally the minimal structure where the definitions make sense is a preorder.

I have placed it in a separate public namespace because of the volume of definitions it adds (to the namespace and to docs) that are not relevant if you are not working with the appropriate kind of relation.

At the moment the properties cover queries useful for preorders, strict/non-strict partial orders, directed sets, and meet/join semilattices, plus a few properties for certain types of lattices.

I expect to submit a PR with more properties for lattices and various subtypes of lattices when I have had the time to test the draft definitions I have. I expect this PR should be easier to review as a consequence.