-- Hello this is a comment

module Demo where

data Bool : Set where
  True : Bool
  False : Bool

not : Bool -> Bool
not True = False
not False = True

if_then_else_ : Bool -> Bool -> Bool -> Bool
if True then t else e = t
if False then t else e = e

data ℕ : Set where
  Zero : ℕ
  Succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
Zero + y = y
Succ x + y = Succ (x + y)

{-# BUILTIN NATURAL ℕ #-}

cond : ∀ {a : Set} -> Bool -> a -> a -> a
cond True t e = t
cond False t e = e

test : ℕ
test = cond True  

id : ∀ {a : Set} -> a -> a 
id x = x

data List (a : Set) : Set where
  Nil : List a 
  Cons : a -> List a -> List a

_++_ : {a : Set} -> List a -> List a -> List a
Nil ++ ys = ys
Cons x xs ++ ys = Cons x (xs ++ ys)

xs : List ℕ
xs = Cons  (Cons  (Cons  Nil))

data Maybe (a : Set) : Set where
  Nothing : Maybe a
  Just : a -> Maybe a

_!!_ : {a : Set} -> List a -> ℕ -> Maybe a
Nil !! Zero = Nothing
Cons x xs !! Zero = Just x
Nil !! Succ i = Nothing
Cons x xs !! Succ i = xs !! i