packages feed

liquidhaskell-0.7.0.0: include/Data/Vector.hquals

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 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)