diff options
| author |  rustanleino <unknown> | 2010-03-31 22:17:44 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-03-31 22:17:44 +0000 |
| commit | a7f7adfb814d4777384b6358e338d1e7b54e8712 (patch) | |
| tree | 416de7a95ec6a32aa1eb7d43b0ec216a5b517d0c /Binaries/DafnyPrelude.bpl | |
| parent | 4622c8070d0c9601dbe2fcdd57f68850f1fbda3f (diff) | |
Dafny:
* Added match statements (in addition to the previous match expressions)
* Added missing axiom about boxes and datatypes
* Improved axioms for datatype rank comparisons
* Added test cases with mutual-recursion termination challenges
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 253cfd12..04da0993 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -174,6 +174,7 @@ axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b); axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b);
axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b);
axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b);
+axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b);
// note: an axiom like this for bool would not be sound
// ---------------------------------------------------------------
|