why3doc index index
Author: Martin Clochard
theory Full
type t predicate le t t clone export relations.PreOrder with type t = t, predicate rel = le, axiom .
Standard preorder theory.
Definable symbols for equality and strict ordering.
predicate eq t t axiom eq_def : forall x y. eq x y <-> le x y /\ le y x predicate lt t t axiom lt_def : forall x y. lt x y <-> le x y /\ not le y x clone relations.Equivalence as Eq with type t = t, predicate rel = eq, lemma Trans, lemma Refl, lemma Symm
Equality is provably an equivalence relation.
clone relations.PartialStrictOrder as Lt with type t = t, predicate rel = lt, lemma Trans, lemma Asymm
Strict ordering is indeed a strict partial order.
end theory TotalFull
clone export Full with axiom . clone export relations.Total with type t = t, predicate rel = le, axiom Total clone relations.Total as Lt with type t = t, predicate rel = le, goal Total lemma lt_def2 : forall x y. lt x y <-> not le y x end module Computable
use int.Int clone export TotalFull with axiom . val compare (x y:t) : int ensures { result > 0 <-> lt y x } ensures { result < 0 <-> lt x y } ensures { result = 0 <-> eq x y }
Comparison is computable.
end
Generated by why3doc 1.7.0