Add higher-order-functions and some other goodies

  * The reads clause now needs to be self framing.

  * The requires clause now needs to be framed by the reads clause.

  * There are one-shot lambdas, with a single arrow, but they will probably be
    removed.

  * There is a {:heapQuantifier} attribute to quantifiers, but they will
    probably be removed.

  * Add smart handling of type variables

  * Add < and > for datatype & type parameter

1 files changed, 1 insertions, 1 deletions

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 703cbaf1..a208b1b6 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -65,7 +65,7 @@ class Node {
     requires if next == null then true else 0 <= 5/x;  // error: ill-defined then branch

     requires if next.next == null then true else true;  // error: ill-defined guard

     requires 10/x != 8;  // this is well-defined, because we get here only if x is non-0

-    reads this;

+    reads this, next;

   {

     12

   }