From bcd9c547b4245b014b1296b9924b4c7b4f4bf02e Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Wed, 2 Feb 2011 23:23:14 +0000
Subject: Dafny: added ensures clauses to functions

---
 Test/dafny0/DTypes.dfy | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'Test/dafny0/DTypes.dfy')

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index c6f0737c..d925587b 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -74,3 +74,16 @@ class Node { }
 
 class CP<T,U> {
 }
+
+datatype Data {
+  Lemon;
+  Kiwi(int);
+}
+
+function G(d: Data): int
+  requires d != #Data.Lemon;
+{
+  match d
+  case Lemon => G(d)
+  case Kiwi(x) => 7
+}
-- 
cgit v1.2.3