From 60036a94bf56dcb15e7f426f0e485e16fb85b651 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Thu, 21 Aug 2014 23:23:20 -0700
Subject: Added .Trunc field to real-based types Changed semantics of
 real-to-int conversions--these now have a precondition that the number
 converted is already an integer

---
 Binaries/DafnyPrelude.bpl | 14 +-------------
 1 file changed, 1 insertion(+), 13 deletions(-)

(limited to 'Binaries/DafnyPrelude.bpl')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 3d5bf111..bf9ef568 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -432,8 +432,7 @@ axiom (forall o: ref :: 0 <= _System.array.Length(o));
 // -- Reals ------------------------------------------------------
 // ---------------------------------------------------------------
 
-function _System.Real.RealToInt(h: Heap, x: real): int { int(x) }
-function _System.Real.IntToReal(h: Heap, x: int): real { real(x) }
+function {:inline true} _System.real.Trunc(x: real): int { int(x) }
 
 // ---------------------------------------------------------------
 // -- The heap ---------------------------------------------------
@@ -868,17 +867,6 @@ axiom (forall<T> s, t: Seq T ::
 function Seq#FromArray(h: Heap, a: ref): Seq Box;
 axiom (forall h: Heap, a: ref ::
   { Seq#Length(Seq#FromArray(h,a)) }
-  /*
-<<<<<<< local
-    Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));
-axiom (forall h: Heap, a: ref :: { Seq#FromArray(h,a): Seq Box }
-   (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));
-axiom (forall<alpha> h: Heap, o: ref, f: Field alpha, v: alpha, a: ref ::
-  { Seq#FromArray(update(h, o, f, v), a) }
-    o != a ==> Seq#FromArray(update(h, o, f, v), a) == Seq#FromArray(h, a) );
-axiom (forall h: Heap, i: int, v: Box, a: ref ::
-=======
-*/
   Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));
 axiom (forall h: Heap, a: ref, i: int ::
   { Seq#Index(Seq#FromArray(h, a): Seq Box, i) }
-- 
cgit v1.2.3