https://github.com/EasyCrypt/easycrypt
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
Fix bug w.r.t. _tools presence detection.
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
Number.ec
(* --------------------------------------------------------------------
* Copyright IMDEA Software Institute / INRIA - 2013, 2014
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
(*
* theory NumTheory.
* op norm : ring -> ring.
* op le : ring -> ring -> bool.
* op lt : ring -> ring -> bool.
*
* axiom ler_norm_add (x y : ring): le (norm (x + y)) (norm x + norm y).
* axiom addr_gt0 (x y : ring): lt zeror x => lt zeror y => lt zeror (x + y).
* axiom norm_eq0 (x : ring): norm x = zeror => x = zeror.
* axiom ger_leVge (x y : ring): le zeror x => le zeror y => (le x y) \/ (le y x).
* axiom normrM (x y : ring): norm (x * y) = norm x * norm y.
* axiom ler_def (x y : ring): le x y <=> (norm (y - x) = y - x).
* axiom ltr_def (x y : ring): lt x y <=> (y <> x) /\ le x y.
* end NumTheory.
*)