Simple1.hs

module Simple1(C) where


data List a   = Nil | Cons a (List a)

-- ?
data TestR a  = TestR { filed1 :: a, field2 :: [a] }

f x = let assert {x > 5} ::: True in 3

data C = Mk



property Any  = Gfp X. X
property None = Lfp X. X

assert All x::Int. x ::: Any
assert Exist x::Int. x ::: None
assert All x::Int. x ::: !even
assert All x::Int. (x ::: !even) \/ x === 1

assert All x. {x::Int} ::: !even ==> -/ (x ::: !odd)
assert A = All x. Exist y. {x::Int} === y  {-#cert:certA#-} {-#cert:certA1#-}

assert B = All xs. {xs::[Int]} ::: !(\xs -> length xs < 3) ==> xs === {[1,2,3,4]}
assert C = All xs. {xs::[Int]} ::: !(\xs -> length xs < 100)

-- signatures in comprahensions don;t yet work in quick check
property AllEven = Gfp X. {| xs :: [Int] | ({xs::[Int]} ::: []) \/ (xs ::: (!even : X)) |}

-- assert D = {[2::Int,4,6,8,10,12]} ::: AllEven
assert E = All xs::[Int]. xs ::: AllEven


assert F = All x::Int. All y. x ::: !(< y) ==> {x + 1} ::: !(<= y)
--assert G = ALl x::Int. x ::: !(const False) ==> undefined

-- assert F = All x::a. x === x