search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
240 stars 33 forks source link

Add support for special-relations #646

Closed LeventErkok closed 1 year ago

LeventErkok commented 1 year ago

z3 supports partial/linear/tree orders; see: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-special-relations

Would be nice to have access to these from SBV.

LeventErkok commented 1 year ago

Done!