diff options
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 3d993797..3f508c81 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -10,6 +10,10 @@ axiom $$Language$Dafny; // coming from a Dafny program. // ---------------------------------------------------------------
// -- Literals ---------------------------------------------------
// ---------------------------------------------------------------
+function {:identity} LitInt(x: int): int { x }
+axiom (forall x: int :: { $Box(LitInt(x)) } $Box(LitInt(x)) == Lit($Box(x)) );
+function {:identity} LitReal(x: real): real { x }
+axiom (forall x: real :: { $Box(LitReal(x)) } $Box(LitReal(x)) == Lit($Box(x)) );
function {:identity} Lit<T>(x: T): T { x }
axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
|