update include

ucsd-progsys · Mar 6, 2017 · bea9d84 · bea9d84
1 parent 949fa0a
commit bea9d84
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/include/GHC/ForeignPtr.spec b/include/GHC/ForeignPtr.spec
@@ -2,8 +2,8 @@ module spec GHC.ForeignPtr where
 
 measure fplen :: GHC.ForeignPtr.ForeignPtr a -> GHC.Types.Int
 
-type ForeignPtrV a   = {v: (GHC.ForeignPtr.ForeignPtr  a) | 0 <= (fplen v)}
-type ForeignPtrN a N = {v: (ForeignPtrV a) | (fplen v) = N }
+type ForeignPtrV a   = {v: GHC.ForeignPtr.ForeignPtr a | 0 <= fplen v}
+type ForeignPtrN a N = {v: GHC.ForeignPtr.ForeignPtr a | 0 <= fplen v && fplen v == N }
 
 mallocPlainForeignPtrBytes :: n:{v:GHC.Types.Int  | v >= 0 } -> (GHC.Types.IO (ForeignPtrN a n))