diff options
| author |  Rustan Leino <unknown> | 2014-02-23 17:27:26 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-23 17:27:26 -0800 |
| commit | d47400c8a1ba72497cc145173aa6ad9f6b1b5a85 (patch) | |
| tree | e7c26059931e9f4c9700de8167e5b3f6269ea07b /Test/dafny3/WideTrees.dfy | |
| parent | 79610237eba7902e8be127fa54f2572a2c01f6b7 (diff) | |
Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -> "prefix lemma")
Diffstat (limited to 'Test/dafny3/WideTrees.dfy')
| -rw-r--r-- | Test/dafny3/WideTrees.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny3/WideTrees.dfy b/Test/dafny3/WideTrees.dfy index e381726e..3fa99256 100644 --- a/Test/dafny3/WideTrees.dfy +++ b/Test/dafny3/WideTrees.dfy @@ -36,12 +36,12 @@ function SmallTrees(n: nat): Stream<Tree> if n == 0 then SNil else SCons(SmallTree(n-1), SmallTrees(n))
}
// prove that the tree returned by SmallTree is finite
-ghost method Theorem(n: nat)
+lemma Theorem(n: nat)
ensures HasBoundedHeight(SmallTree(n));
{
Lemma(n);
}
-comethod Lemma(n: nat)
+colemma Lemma(n: nat)
ensures LowerThan(SmallTrees(n), n);
{
if 0 < n {
|