33 lines
645 B
Agda
33 lines
645 B
Agda
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
|