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 | 803f42612314d2d27f20dfa476bf0ff8ed24d958 (patch) | |
| tree | f341d7239381047f31d761938df3b9e1f7a3874c /Test/dafny0/NatTypes.dfy | |
| parent | e1bf8c0bfff274a0651fb581951cfcaae8b34007 (diff) | |
Dafny: permanently changed the syntax of "datatype" declarations to what previously was an alternative syntax
Diffstat (limited to 'Test/dafny0/NatTypes.dfy')
| -rw-r--r-- | Test/dafny0/NatTypes.dfy | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index e4d0cbe7..53d3bf03 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -44,7 +44,7 @@ method Generic<T>(i: int, t0: T, t1: T) returns (r: T) { function method FenEric<T>(t0: T, t1: T): T;
-datatype Pair<T> { Pr(T, T); }
+datatype Pair<T> = Pr(T, T);
method K(n: nat, i: int) {
match (Pair.Pr(n, i)) {
@@ -55,10 +55,7 @@ method K(n: nat, i: int) { }
}
-datatype List<T> {
- Nil;
- Cons(nat, T, List<T>);
-}
+datatype List<T> = Nil | Cons(nat, T, List<T>);
method MatchIt(list: List<object>) returns (k: nat)
{
|