From 454909184e73582e425cad56a526956d91b88dcc Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Thu, 14 May 2015 15:44:39 -0700
Subject: 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) }

---
 Test/dafny0/NestedMatch.dfy.expect | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 Test/dafny0/NestedMatch.dfy.expect

(limited to 'Test/dafny0/NestedMatch.dfy.expect')

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
-- 
cgit v1.2.3