From 84bd33b3b99377f139dd60aaeb15f5e03b0c56b3 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Thu, 3 Feb 2011 02:27:13 +0000
Subject: Dafny: replaced the user-defined $ite function with Boogie's built-in
 if-then-else expression

---
 Binaries/DafnyPrelude.bpl | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'Binaries/DafnyPrelude.bpl')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 8795d6a5..6c9faa29 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -178,14 +178,6 @@ axiom (forall<T> s, t: Seq T ::
   Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s &&
   Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);
 
-// ---------------------------------------------------------------
-// -- If then else -----------------------------------------------
-// ---------------------------------------------------------------
-
-function $ite<T>(bool, T, T): T;
-axiom (forall<T> g: bool, a,b: T :: { $ite(g,a,b) }
-  (g ==> $ite(g,a,b) == a) && (!g ==> $ite(g,a,b) == b));
-
 // ---------------------------------------------------------------
 // -- Boxing and unboxing ----------------------------------------
 // ---------------------------------------------------------------
-- 
cgit v1.2.3