diff options
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 3 |
1 files changed, 3 insertions, 0 deletions
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);
|