package gospel

  1. Overview
  2. Docs
A tool-agnostic formal specification language for OCaml

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

  1. J
    Jean-Christophe Filliâtre
  2. S
    Samuel Hym
  3. C
    Cláudio Lourenço
  4. N
    Nicolas Obsorne
  5. C
    Clément Pascutto
  6. M
    Mário Pereira

Maintainers

  1. J
    Jean-Christophe.Filliatre@lri.fr

Sources

v0.3.1.tar.gz
md5=99432da6253cc1d5eb071caa635044a1
sha512=a50035d28c10119b0d42391fcf1cce4cab101170f6ed308bfd214165b09e595d817fc0eea0efb4632810bd962cad022473ff9148bccd4854e46c22462347702e

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))