liquidhaskell-0.1: include/Data/Vector.spec

module spec Data.Vector where

import GHC.Base

measure vlen    :: forall a. (Vector a) -> Int

invariant       {v: Vector a | (vlen v) >= 0 } 

assume !        :: forall a. x:(Vector a) -> vec:{v: Int | ((0 <= v) && (v < (vlen x))) } -> a 

assume fromList :: forall a. x:[a] -> {v: Vector a  | (vlen v) = (len x) }

assume length   :: forall a. x:(Vector a) -> {v: Int | (v = (vlen x) && v >= 0) }