module CaseEval

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

plus : Nat -> Nat -> Nat
plus Z y = y
plus (S x) y = S (plus x y)

data Eq : {A : U} -> A -> A -> U where
  Refl : {A : U} -> {x : A} -> Eq x x

two : Eq (plus (S Z) (S Z)) (S (S Z))
two = Refl

three : Eq (plus (S Z) (S (S Z))) (plus (S (S Z)) (S Z))
three = Refl

addZero : {n : Nat} -> Eq (plus Z n) n
addZero {n} = Refl

infixr 1 _,_
data Pair : U -> U -> U where
  _,_ : {A B : U} -> A -> B -> Pair A B

fst : {A B : U} -> Pair A B -> A
fst (a,b) = a

-- I had an ordering issue, but it didn't show up with only one constructor argument
test : Eq (fst (Z, S Z)) Z
test = Refl