From aec9290fbd3ca9ada5a7fad4dabb4ed1ffad6a84 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Mon, 28 Sep 2015 13:31:26 -0700
Subject: Additional tests

---
 Test/dafny0/CoPrefix.dfy | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

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

diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy
index 0becb24d..3b6bd670 100644
--- a/Test/dafny0/CoPrefix.dfy
+++ b/Test/dafny0/CoPrefix.dfy
@@ -192,3 +192,35 @@ module Recursion {
     }
   }
 }
+
+module PrefixEquality {
+  codatatype Stream<T> = Cons(head: T, Stream)
+    
+  colemma Test0(s: Stream, t: Stream)
+    requires s.head == t.head
+  {
+    calc {
+      s;
+      ==#[_k-1]
+      t;  // error: this step might not hold
+      ==#[if 2 <= _k then _k-2 else _k-1]
+      s;  // error: this step might not hold
+      ==#[0]
+      t;
+    }
+  }
+
+  colemma Test1(s: Stream, t: Stream)
+    requires s == t
+  {
+    calc {
+      s;
+      ==#[_k-1]
+      t;
+      ==#[_k-2]  // error: prefix-equality limit must be at least 0
+      s;
+      ==#[0]
+      t;
+    }
+  }
+}
-- 
cgit v1.2.3