diff options
| author |  Rustan Leino <unknown> | 2014-07-11 20:50:08 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-07-11 20:50:08 -0700 |
| commit | a8161c0e52d9c1743679091c36f64e925723d607 (patch) | |
| tree | 01d7b64cc2c85b81452e3aceba4318f6c1e68353 /Test/dafny0/TypeSynonyms.dfy | |
| parent | 92cced2f7bde488e450fa12f7ef50d98f474ab61 (diff) | |
Added type synonyms. (No support yet for these in refinements.)
Diffstat (limited to 'Test/dafny0/TypeSynonyms.dfy')
| -rw-r--r-- | Test/dafny0/TypeSynonyms.dfy | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/Test/dafny0/TypeSynonyms.dfy b/Test/dafny0/TypeSynonyms.dfy new file mode 100644 index 00000000..4bec5253 --- /dev/null +++ b/Test/dafny0/TypeSynonyms.dfy @@ -0,0 +1,46 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+type MyType<A> = int
+
+type Int = int
+
+type PairaBools = (bool, bool)
+
+datatype List<T> = Nil | Cons(T, List)
+
+type Synonym0<T,U> = List<T>
+
+type Synonym1<T> = List // type argument of List filled in automatically
+
+type Synonym2<A> = List<A>
+
+type Synonym3<B> = Synonym4
+
+type Synonym4<C> = Synonym2<C>
+
+type Synonym5<A,B> = List
+
+function Plus(x: Int, y: int): Int
+{
+ x + y
+}
+
+method Next(s: Synonym1) returns (u: Synonym1)
+{
+ match s
+ case Nil => u := Nil;
+ case Cons(_, tail) => u := tail;
+}
+
+method Add<W>(t: W, s: Synonym1) returns (u: Synonym1)
+{
+ u := Cons(t, Nil);
+}
+
+function Skip(s: Synonym3): Synonym0
+{
+ match s
+ case Nil => Nil
+ case Cons(_, tail) => tail
+}
|