NMake (and hence BigN): shiftr, shiftl now in the signature NSig

 we export the "safe" version of these functions, working for all
 input and not only reasonably small shifting arg. The former
 "unsafe" shiftr and shiftl are now unsafe_shiftr and unsafe_shiftl.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12688 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 0 deletions

diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 116927766..85639aa6a 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -55,6 +55,9 @@ Module Type NType.
  Parameter div : t -> t -> t.
  Parameter modulo : t -> t -> t.
  Parameter gcd : t -> t -> t.
+ Parameter shiftr : t -> t -> t.
+ Parameter shiftl : t -> t -> t.
+ Parameter is_even : t -> bool.
 
  Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
  Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
@@ -76,6 +79,10 @@ Module Type NType.
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
  Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
  Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
+ Parameter spec_shiftr: forall p x, [shiftr p x] = [x] / 2^[p].
+ Parameter spec_shiftl: forall p x, [shiftl p x] = [x] * 2^[p].
+ Parameter spec_is_even: forall x,
+  if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1.
 
 End NType.