module ICFPPrelude where

postulate Level : Set
          lz    : Level
{-# BUILTIN LEVEL Level #-}
{-# BUILTIN LEVELZERO lz #-}

record  : Set where
  constructor ⟨⟩

data  : Set where

¬_ : Set  Set
¬_ A = A  

data Nat : Set where
  zero : Nat
  suc  : Nat  Nat

{-# BUILTIN NATURAL Nat  #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

_+_ : Nat  Nat  Nat
zero + n = n
suc m + n = suc (m + n)

infixr 2 _∪_
data _∪_ A B : Set where
  inl : A  A  B
  inr : B  A  B

data _≡_ {a}{A : Set a}(x : A) : A  Set a where
  refl : x  x

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}