diff options
| author |  rustanleino <unknown> | 2010-11-01 21:56:14 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-11-01 21:56:14 +0000 |
| commit | 385c5b3011cebd4c296a86cd1e5c2258afda98ba (patch) | |
| tree | 9bc2d8a8b92535a2316c900daddb00c23d1150b9 /Binaries | |
| parent | 3bf8b18954dfba54b0bf42072004f0e5dabc2bcf (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 -------------------------------------------------
// ---------------------------------------------------------------
|