1 files changed, 59 insertions, 0 deletions
diff --git a/Test/dafny0/NestedMatch.dfy b/Test/dafny0/NestedMatch.dfy
new file mode 100644
index 00000000..81319b4a
--- /dev/null
+++ b/Test/dafny0/NestedMatch.dfy
@@ -0,0 +1,59 @@
+// RUN: %dafny /compile:0  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Nat = Zero | Suc(Nat)
+
+predicate Even(n: Nat)
+{
+  match n
+  case Zero => true
+  case Suc(Zero) => false
+  case Suc(Suc(p)) => Even(p)
+}
+
+
+method checkEven(n: Nat) {
+  assert Even(Zero) == true;
+  assert Even(Suc(Zero)) == false;
+  assert Even(Suc(Suc(n))) == Even(n);
+}
+
+datatype List<T> = Nil | Cons(T, List<T>)
+
+function last<T>(xs: List<T>): T
+  requires xs != Nil
+{
+  match xs
+  case Cons(y, Nil) => y
+  case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
+}
+
+method checkLast<T>(y: T) {
+  assert last(Cons(y, Nil)) == y;
+  assert last(Cons(y, Cons(y, Nil))) == last(Cons(y, Nil));
+}
+
+
+function minus(x: Nat, y: Nat): Nat
+{
+  match (x, y)
+  case (Zero, _) => Zero
+  case (Suc(_), Zero) => x
+  case (Suc(a), Suc(b)) => minus(a, b)
+}
+
+method checkMinus(x:Nat, y: Nat) {
+  assert minus(Suc(x), Suc(y)) == minus(x,y);
+}
+
+
+// nested match statement
+method Last<T>(xs: List<T>) returns (x: T)
+  requires xs != Nil
+{
+ 
+  match xs {
+  	case Cons(y, Nil) => x:= y;
+  	case Cons(y, Cons(z, zs)) => x:=Last(Cons(z, zs));
+  }
+}