package gospel
A tool-agnostic formal specification language for OCaml
Install
Dune Dependency
Authors
Maintainers
Sources
0.3.0.tar.gz
md5=e5b7f601526cbf590a070b6b9aebe1ad
sha512=a1375603a3f0ac7681e7e2e989be8af809edef78becc7d920e1d18af4f1db576dce91525cec70292c4ba559eb3f3bac67b023bcc826ea3dfdab956c86990ef91
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))