diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN/NMake_gen.ml')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 22a4b200a2..534b680e2a 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -79,8 +79,9 @@ let _ = pr "Require Import Nbasic."; pr "Require Import Wf_nat."; pr "Require Import StreamMemo."; + pr "Require Import NSig."; pr ""; - pr "Module Make (Import W0:CyclicType)."; + pr "Module Make (Import W0:CyclicType) <: NType."; pr ""; pr " Definition w0 := W0.w."; @@ -163,8 +164,13 @@ let _ = pr " Open Scope Z_scope."; pr " Notation \"[ x ]\" := (to_Z x)."; - pr " "; + pr ""; + pr " Definition to_N x := Zabs_N (to_Z x)."; + pr ""; + + pr " Definition eq x y := (to_Z x = to_Z y)."; + pr ""; pp " (* Regular make op (no karatsuba) *)"; pp " Fixpoint nmake_op (ww:Type) (ww_op: znz_op ww) (n: nat) : "; @@ -1315,6 +1321,12 @@ let _ = pr " comparenm)."; pr ""; + pr " Definition lt n m := compare n m = Lt."; + pr " Definition le n m := compare n m <> Gt."; + pr " Definition min n m := match compare n m with Gt => m | _ => n end."; + pr " Definition max n m := match compare n m with Lt => m | _ => n end."; + pr ""; + for i = 0 to size do pp " Let spec_compare_%i: forall x y," i; pp " match compare_%i x y with " i; @@ -2396,7 +2408,6 @@ let _ = pr " end."; pr ""; - pr " Theorem spec_of_N: forall x,"; pr " [of_N x] = Z_of_N x."; pa " Admitted."; |