diff options
Diffstat (limited to 'Test/dafny1/Rippling.dfy')
| -rw-r--r-- | Test/dafny1/Rippling.dfy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index 211afd83..677e6e70 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -278,11 +278,11 @@ function mirror(t: Tree): Tree // Function parameters
// Dafny currently does not support passing functions as arguments. To simulate
-// arbitrary functions, the following type (declared as a class) and Apply function
-// play the role of applying some prescribed function (here, an instance of the class)
+// arbitrary functions, the following type and Apply function play the role of
+// applying some prescribed function (here, a value of the type)
// to some argument.
-class FunctionValue { }
+type FunctionValue;
function Apply(f: FunctionValue, x: Nat): Nat // this function is left uninterpreted
// The following functions stand for the constant "false" and "true" functions,
|