package gospel
A tool-agnostic formal specification language for OCaml
Install
Dune Dependency
Authors
Maintainers
Sources
0.2.0.tar.gz
md5=964e7cb82b4391c7ad0794c20adcc67f
sha512=15c5d3f48fac648ce0799c2664323d461f3792ae9477ba0fe8c499228a9faddda22e8ef66ef10733dce550dcf8ba2641fce2b5472005f649f28e5426d0631375
doc/gospel.stdlib/Gospelstdlib/Order/index.html
Module Gospelstdlib.Order
Gospel declaration:
predicate is_pre_order (cmp: 'a -> 'a -> int) =
(forall x. cmp x x = 0) /\
(forall x y. cmp x y <= 0 <-> cmp y x >= 0) /\
(forall x y z.
(cmp x y <= 0 -> cmp y z <= 0 -> cmp x z <= 0) /\
(cmp x y <= 0 -> cmp y z < 0 -> cmp x z < 0) /\
(cmp x y < 0 -> cmp y z <= 0 -> cmp x z < 0) /\
(cmp x y < 0 -> cmp y z < 0 -> cmp x z < 0))