diff options
author | Rustan Leino <leino@microsoft.com> | 2012-10-04 00:02:43 -0700 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2012-10-04 00:02:43 -0700 |
commit | 86da04e8be269d13874191c81cee0e2110d6373e (patch) | |
tree | 3e179711e6f621ff10bbea22fbcaa9f0e9d62e47 /Binaries | |
parent | 0cf1c052a1b3f89384a6c859fc8680851b6edce0 (diff) | |
parent | 17a14997cbcdad8bb0a435cf48dfb783ea21f3ac (diff) |
Merge
Diffstat (limited to 'Binaries')
-rw-r--r-- | Binaries/DafnyPrelude.bpl | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index e6d05bea..fafc9484 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -647,18 +647,3 @@ type TickType; var $Tick: TickType;
// ---------------------------------------------------------------
-// -- Arithmetic -------------------------------------------------
-// ---------------------------------------------------------------
-
-// the connection between % and /
-axiom (forall x:int, y:int :: {x % y} {x / y} x % y == x - x / y * y);
-
-// remainder is always Euclidean Modulus.
-axiom (forall x:int, y:int :: {x % y} 0 < y ==> 0 <= x % y && x % y < y);
-axiom (forall x:int, y:int :: {x % y} y < 0 ==> 0 <= x % y && x % y < -y);
-
-// the following axiom has some unfortunate matching, but it does state a property about % that
-// is sometimes useful
-axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);
-
-// ---------------------------------------------------------------
|