From bf6de3d13197e1635a4d9fe807b3f4b45113ae6a Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Tue, 21 Oct 2014 01:16:56 -0700
Subject: Comparisons and well-founded order of char

---
 Binaries/DafnyPrelude.bpl | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 4cdb21e9..9b410b1e 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -79,6 +79,9 @@ axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
 type char;
 function char#FromInt(int): char;
 function char#ToInt(char): int;  // inverse of char#FromInt
+axiom (forall ch: char ::
+  { char#ToInt(ch) } 
+  char#FromInt(char#ToInt(ch)) == ch);
 axiom (forall n: int ::
   { char#FromInt(n) }
   0 <= n && n < 65536 ==> char#ToInt(char#FromInt(n)) == n);
-- 
cgit v1.2.3