liquid-vector 0.13.1.0.1 → 0.13.1.0.2
raw patch · 2 files changed
+13/−13 lines, 2 filesdep ~liquidhaskell
Dependency ranges changed: liquidhaskell
Files
- liquid-vector.cabal +2/−2
- src/Data/Vector_LHAssumptions.hs +11/−11
liquid-vector.cabal view
@@ -1,6 +1,6 @@ cabal-version: 1.24 name: liquid-vector-version: 0.13.1.0.1+version: 0.13.1.0.2 synopsis: LiquidHaskell specs for the vector package description: LiquidHaskell specs for the vector package. license: BSD3@@ -20,7 +20,7 @@ hs-source-dirs: src build-depends: base < 5 , vector >= 0.13.1.0 && < 0.14- , liquidhaskell >= 0.9.2.8+ , liquidhaskell >= 0.9.12.2.1 default-language: Haskell2010 default-extensions: PackageImports if impl(ghc >= 8.10)
src/Data/Vector_LHAssumptions.hs view
@@ -30,18 +30,18 @@ assume Data.Vector.head :: forall a. {xs: Data.Vector.Vector a | vlen xs > 0} -> a -qualif VecEmpty(v: Data.Vector.Vector a) : (vlen v) = 0-qualif VecEmpty(v: Data.Vector.Vector a) : (vlen v) > 0-qualif VecEmpty(v: Data.Vector.Vector a) : (vlen v) >= 0+qualif VecEmpty(v: Data.Vector.Vector a) { vlen v = 0 }+qualif VecEmpty(v: Data.Vector.Vector a) { vlen v > 0 }+qualif VecEmpty(v: Data.Vector.Vector a) { vlen v >= 0 } -qualif Vlen(v:int, x: Data.Vector.Vector a) : (v = vlen x)-qualif Vlen(v:int, x: Data.Vector.Vector a) : (v <= vlen x)-qualif Vlen(v:int, x: Data.Vector.Vector a) : (v < vlen x)+qualif Vlen(v:int, x: Data.Vector.Vector a) { v = vlen x }+qualif Vlen(v:int, x: Data.Vector.Vector a) { v <= vlen x }+qualif Vlen(v:int, x: Data.Vector.Vector a) { v < vlen x } -qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v < vlen x)-qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v <= vlen x)-qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v > vlen x)-qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v >= vlen x)-qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v = vlen x)+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) { vlen v < vlen x }+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) { vlen v <= vlen x }+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) { vlen v > vlen x }+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) { vlen v >= vlen x }+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) { vlen v = vlen x } @-}