{-@ LIQUID "--totality" @-}
{-# LANGUAGE EmptyDataDecls #-}
module BoolMeasure where
import Prelude hiding (length)
{-@ myhead :: {v:[a] | nonEmpty v} -> a @-}
myhead (x:_) = x
{-@ measure nonEmpty @-}
nonEmpty (x:xs) = True
nonEmpty [] = False
{-@ measure length @-}
length :: [a] -> Int
length (x:xs) = 1 + length xs
length [] = 0
{-@ measure lenEqFive @-}
lenEqFive (x:xs) = length xs == 4
lenEqFive [] = False
{-@ measure lenNEqFive @-}
lenNEqFive (x:xs) = not (length xs == 4)
lenNEqFive [] = True
{-@ measure lenGEFour @-}
lenGEFour (x:xs) = length xs >= 3
lenGEFour [] = False
{-@ len3 :: {v:[Int] | (not (lenEqFive v))} @-}
len3 :: [Int]
len3 = [1, 2, 3]
{-@ len5 :: {v:[Int] | (lenEqFive v) && (lenGEFour v) } @-}
len5 :: [Int]
len5 = [1, 2, 3, 4, 5]
{-@ measure length @-}
{-@ foo :: x:[a] -> {v: Bool | v <=> (nonEmpty x) } @-}
foo :: [a] -> Bool
foo x = nonEmpty x
cons = (:)
nil = []