module TestCase2

data Nat : U where
  Z : Nat
  S : Nat -> Nat

plus : Nat -> Nat -> Nat
plus Z m = m
-- if this is a capital K on LHS, it fails with a poor error message
plus (S k) m = S (plus k m)

-- -- Example from Jesper talk (translated to case tree)
max : Nat -> Nat -> Nat
max Z m = m
max n Z = n
max (S k) (S l) = S (max k l)

data List : U -> U where
  LN : {a : U} -> List a
  LCons : {a : U} -> a -> List a -> List a

data Vect : Nat -> U -> U where
  Nil : {a : U} -> Vect Z a
  Cons : {a : U} {n : Nat} -> a -> Vect n a -> Vect (S n) a

-- NEXT Need to handle implicits
-- I've hacked implicits, but need to figure out indices..
length : {a : U} {n : Nat} -> Vect n a -> Nat
length Nil = Z
length (Cons x xs) = S (length xs)

data Unit : U where
  MkUnit : Unit

-- This should fail (and does!)
-- bar : Vect (S Z) Unit
-- bar = (Cons MkUnit (Cons MkUnit Nil))

data Bool : U where
  True : Bool
  False : Bool

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


not2 : Bool -> Bool
not2 True = False
not2 x = True

-- TEST CASE - remove second clause here and expect error
and : Bool -> Bool -> Bool
and True y = y
and False _ = False

nand : Bool -> Bool -> Bool
nand x y = not (case x of
    True => y
    False => False)


-- for stuff like this, we should add Agda () and check for no constructors
data Void : U where

SnocList : U -> U
SnocList a = List a