module spec Data.Either where

// invariant {v:[Data.Either.Either a b] | (lenRight v >= 0) && (lenRight v <= len v)}

// measure lenRight :: [Data.Either.Either a b] -> GHC.Types.Int
// lenRight (x:xs) = if (isLeft x) then (lenRight xs) else (lenRight xs + 1)
// lenRight ([])   = 0

// measure isLeftHd :: [Data.Either.Either a b] -> Bool 
// isLeftHd (x:xs) = (isLeft x)
// isLeftHd ([])   = false

measure isLeft :: Data.Either.Either a b -> Bool
isLeft (Left x)  = true
isLeft (Right x) = false
