Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -> "prefix lemma")

1 files changed, 3 insertions, 3 deletions

diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
index b31dc5be..27b279c3 100644
--- a/Test/dafny0/Coinductive.dfy
+++ b/Test/dafny0/Coinductive.dfy
@@ -133,7 +133,7 @@ module CoPredicateResolutionErrors {
 

 // --------------------------------------------------

 

-module UnfruitfulCoMethodConclusions {

+module UnfruitfulCoLemmaConclusions {

   codatatype Stream<T> = Cons(head: T, tail: Stream);

 

   copredicate Positive(s: Stream<int>)

@@ -141,13 +141,13 @@ module UnfruitfulCoMethodConclusions {
     s.head > 0 && Positive(s.tail)

   }

 

-  comethod BadTheorem(s: Stream)

+  colemma BadTheorem(s: Stream)

     ensures false;

   {

     BadTheorem(s.tail);

   }

 

-  comethod CM(s: Stream<int>)

+  colemma CM(s: Stream<int>)

     ensures true && !false;

     ensures s.head == 8 ==> Positive(s);

     ensures s.tail == s;