Allowing dangling hints in calculations.

1 files changed, 20 insertions, 1 deletions

diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
index 54a9a3d4..59191ac3 100644
--- a/Test/dafny0/Calculations.dfy
+++ b/Test/dafny0/Calculations.dfy
@@ -60,4 +60,23 @@ function CalcTest3(s: seq<int>): int {
 		|s|;
 	}
 	s[0]
-}
\ No newline at end of file
+}
+
+// dangling hints:
+method CalcTest4(s: seq<int>) 
+	requires forall n | n in s :: n > 0;
+{
+	calc {
+		1 + 1;
+		{ assert 1 + 1 == 2; }
+	}
+	calc {
+		2;
+		{ assert s[0] > 0; } // error: ill-formed hint
+	}
+	calc {
+		|s| > 0;
+	==> { assert s[0] > 0; } // okay
+	}
+	
+}