Allow MatchExpr and MatchStmt to have nested patterns. Such as

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))
}
And
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)
}

1 files changed, 2 insertions, 0 deletions

diff --git a/Test/dafny0/NestedMatch.dfy.expect b/Test/dafny0/NestedMatch.dfy.expect
new file mode 100644
index 00000000..f3a9c95f
--- /dev/null
+++ b/Test/dafny0/NestedMatch.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 11 verified, 0 errors