diff options
| author |  Rustan Leino <unknown> | 2014-01-03 13:22:35 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-01-03 13:22:35 -0800 |
| commit | 07eb4927283f945465e3a2462d89dc865c543c97 (patch) | |
| tree | acfdf3e86c84e01a9f708df686157f1668a4bcbc /Binaries/DafnyPrelude.bpl | |
| parent | 6cdef59ade53baddabf304a3ada5294a2bfdc99c (diff) | |
Print and translate "match" expressions in general positions, not just at the top-level of function bodies. (Note, resolver also needs to allow this before the user can take advantage of this.)
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index d4e7575e..8e18f229 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -479,6 +479,7 @@ axiom (forall<U, V> m: Map U V, m': Map U V :: // ---------------------------------------------------------------
type BoxType;
+const $ArbitraryBoxValue: BoxType;
function $Box<T>(T): BoxType;
function $Unbox<T>(BoxType): T;
|