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, 3 insertions, 3 deletions

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index f484c397..377865fe 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -346,21 +346,21 @@ class DefaultDecreasesFunction {
   }

   function F(x: int): int

     requires Valid();

-    reads Repr;

+    reads this, Repr;

     // the default reads clause is: decreases Repr, x

   {

     if next == null || x < 0 then x else next.F(x + data)

   }

   function G(x: int): int

     requires Valid();

-    reads Repr;

+    reads this, Repr;

     decreases x;

   {

     if next == null || x < 0 then x else next.G(x + data)  // error: failure to reduce 'decreases' measure

   }

   function H(x: int): int

     requires Valid() && 0 <= x;

-    reads Repr;

+    reads this, Repr;

     // the default reads clause is: decreases Repr, x

   {

     if next != null then