#include "../prelude/prelude.ncc"

query add0 = add (succ zero) zero (succ zero)

query add1 = succ zero ++ zero == succ zero

query add2 = exists A : natural . add (succ zero) zero A

query add3 = any $ add (succ zero) zero

query findSat1 = succ zero =< succ (succ zero)

query findSat2 = succ zero =< succ (succ zero) /\ zero =< succ (succ zero)

query findSat0 = free A : natural . A =:= zero


defn ismain : prop 
  as run $ do 
         , putStr "hey!\n"
         , readLine (\A . do 
   	 , putStr A
         , putStr "\nbye!\n")

query main = ismain