diff options
author | leino <unknown> | 2015-09-28 13:31:26 -0700 |
---|---|---|
committer | leino <unknown> | 2015-09-28 13:31:26 -0700 |
commit | aec9290fbd3ca9ada5a7fad4dabb4ed1ffad6a84 (patch) | |
tree | f1f8515675b958c319b94cee89d53422cf6053ff /Test/dafny0/CoPrefix.dfy | |
parent | 4c21d765625b35eab9f5dc4ca21f170d3f7a2f04 (diff) |
Additional tests
Diffstat (limited to 'Test/dafny0/CoPrefix.dfy')
-rw-r--r-- | Test/dafny0/CoPrefix.dfy | 32 |
1 files changed, 32 insertions, 0 deletions
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;
+ }
+ }
+}
|