https://github.com/EasyCrypt/easycrypt
Revision 997d5d4ea162b2e72e1861a70d710c8e4e149e50 authored by Benjamin Gregoire on 19 June 2014, 07:49:50 UTC, committed by Benjamin Gregoire on 19 June 2014, 07:49:50 UTC
1 parent 8bc5765
Tip revision: 997d5d4ea162b2e72e1861a70d710c8e4e149e50 authored by Benjamin Gregoire on 19 June 2014, 07:49:50 UTC
Fix theory IRing
Fix theory IRing
Tip revision: 997d5d4
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.
*)
Computing file changes ...
