Define $Is and $IsAlloc predicates for newtypes.

1 files changed, 2 insertions, 2 deletions

diff --git a/Test/dafny0/DerivedTypes.dfy b/Test/dafny0/DerivedTypes.dfy
index 3345b709..5b3b7d5c 100644
--- a/Test/dafny0/DerivedTypes.dfy
+++ b/Test/dafny0/DerivedTypes.dfy
@@ -57,7 +57,7 @@ module Constraints {
   {

     x % 2 == 0

   }

-  newtype G = x: int where IsEven(x)  // it's okay to use ghost constructs in type constraints

+//  newtype G = x: int where IsEven(x)  // it's okay to use ghost constructs in type constraints

 

   newtype N = nat

 

@@ -69,7 +69,7 @@ module Constraints {
   newtype Te = x: int where 0 <= x < 3 && [5, 7, 8][x] % 2 != 0

 

   newtype Ta = x: int where 0 <= x < 3

-//  newtype Tb = y: Ta where [5, 7, 8][int(y)] % 2 != 0  // the indexing is okay, because of the type constraint for Ta

+  newtype Tb = y: Ta where [5, 7, 8][int(y)] % 2 != 0  // the indexing is okay, because of the type constraint for Ta

 

   newtype Odds = x: int where x % 2 == 1  // error: cannot find witness