diff options
| author |  rustanleino <unknown> | 2010-11-01 21:56:14 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-11-01 21:56:14 +0000 |
| commit | 31f5a7c20e25225e4b9dca95e60e955402f64df6 (patch) | |
| tree | a8b2a54790d1e1900ed0a7ea8d00bd6faa7ce31f /Binaries | |
| parent | 1219dc1f931e17918d3a1bfe580149b21493a0c4 (diff) | |
Dafny: a partial first crack at a Dafny model-viewer provider, including captureState mark-ups in the Boogie code generated from Dafny
Diffstat (limited to 'Binaries')
| -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 476a6bd9..5675d2a1 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -4,6 +4,9 @@ // Edited sequence axioms 20 October 2009 by Alex Summers.
// Copyright (c) 2008-2010, Microsoft.
+const $$Language$Dafny: bool; // To be recognizable to the ModelViewer as
+axiom $$Language$Dafny; // coming from a Dafny program.
+
// ---------------------------------------------------------------
// -- References -------------------------------------------------
// ---------------------------------------------------------------
|