diff options
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 5d0b647f..349da0fd 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -8,6 +8,12 @@ const $$Language$Dafny: bool; // To be recognizable to the ModelViewer as axiom $$Language$Dafny; // coming from a Dafny program.
// ---------------------------------------------------------------
+// -- Literals ---------------------------------------------------
+// ---------------------------------------------------------------
+function {:identity} Lit<T>(x: T): T { x }
+axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
+
+// ---------------------------------------------------------------
// -- References -------------------------------------------------
// ---------------------------------------------------------------
|