diff options
| author |  Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-31 17:13:35 -0700 |
|---|---|---|
| committer | Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-31 17:13:35 -0700 |
| commit | 57a7fa3aa01ced1943dde6fe3270c62f1b6923c3 (patch) | |
| tree | 35d0616be8e25e644a9283732b17e87ed1c17e35 /Binaries/DafnyPrelude.bpl | |
| parent | df71b461ff9284991c06b04d17b6e6b50f8151ae (diff) | |
Dafny: Added map comprehensions and updated display syntax
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 09b6efcf..742fd4e4 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -371,6 +371,15 @@ axiom (forall<U, V> u: U :: { Map#Domain(Map#Empty(): Map U V)[u] }
!Map#Domain(Map#Empty(): Map U V)[u]);
+function Map#Glue<U, V>([U] bool, [U]V): Map U V;
+axiom (forall<U, V> a: [U] bool, b:[U]V ::
+ { Map#Domain(Map#Glue(a, b)) }
+ Map#Domain(Map#Glue(a, b)) == a);
+axiom (forall<U, V> a: [U] bool, b:[U]V ::
+ { Map#Elements(Map#Glue(a, b)) }
+ Map#Elements(Map#Glue(a, b)) == b);
+
+
//Build is used in displays, and for map updates
function Map#Build<U, V>(Map U V, U, V): Map U V;
/*axiom (forall<U, V> m: Map U V, u: U, v: V ::
|