content: 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
  