diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-27 01:44:26 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-27 01:44:26 -0700 |
| commit | 065fa79887779fbfbc14700744acd684c59aa3ec (patch) | |
| tree | bfa784eeee8bbea39c3820b5cf5c0cf1022f0fec /Test/dafny0/FunctionSpecifications.dfy | |
| parent | 9a714cafa2e4d6551f28c57187c28333cc155527 (diff) | |
Dafny: permanently changed the syntax of "datatype" declarations to what previously was an alternative syntax
Diffstat (limited to 'Test/dafny0/FunctionSpecifications.dfy')
| -rw-r--r-- | Test/dafny0/FunctionSpecifications.dfy | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/Test/dafny0/FunctionSpecifications.dfy b/Test/dafny0/FunctionSpecifications.dfy index 21ce5468..13171c47 100644 --- a/Test/dafny0/FunctionSpecifications.dfy +++ b/Test/dafny0/FunctionSpecifications.dfy @@ -6,10 +6,7 @@ function Fib(n: int): int Fib(n-2) + Fib(n-1)
}
-datatype List {
- Nil;
- Cons(int, List);
-}
+datatype List = Nil | Cons(int, List);
function Sum(a: List): int
ensures 0 <= Sum(a);
|