Start of derived types (aka "new types")

Fixed bug in type checking for integer division.

1 files changed, 8 insertions, 1 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 50628438..e0c37e2a 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1101,7 +1101,7 @@ method TraitSynonym()
   var x := new JJ;  // error: new cannot be applied to a trait

 }

 

-// ----- set comprehensions where the term type is finite ----

+// ----- set comprehensions where the term type is finite -----

 

 module ObjectSetComprehensions {

   // allowed in non-ghost context:

@@ -1114,3 +1114,10 @@ module ObjectSetComprehensions {
 

   method D() { var x := set o : object | true :: o; }

 }

+

+// ------ regression test for type checking of integer division -----

+

+method IntegerDivision(s: set<bool>)

+{

+  var t := s / s;  // error: / cannot be used with sets

+}