Steve Dunham
9e72ed67fc
- move over to env for unify et al - fix issue where constraint had short context - drop parameters block - make it clear where context is being used
40 lines
847 B
Agda
40 lines
847 B
Agda
module Concat
|
|
|
|
data Nat : U where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
infixl 7 _+_
|
|
_+_ : Nat -> Nat -> Nat
|
|
Z + m = m
|
|
S n + m = S (n + m)
|
|
|
|
infixr 3 _::_
|
|
data List : U -> U where
|
|
Nil : {A : U} -> List A
|
|
_::_ : {A : U} -> A -> List A -> List A
|
|
|
|
length : {A : U} -> List A -> Nat
|
|
length Nil = Z
|
|
length (x :: xs) = S (length xs)
|
|
|
|
infixl 2 _++_
|
|
|
|
_++_ : {A : U} -> List A -> List A -> List A
|
|
Nil ++ ys = ys
|
|
x :: xs ++ ys = x :: (xs ++ ys)
|
|
|
|
infixl 1 _≡_
|
|
data _≡_ : {A : U} -> A -> A -> U where
|
|
Refl : {A : U} {a : A} -> a ≡ a
|
|
|
|
replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
|
|
replace p Refl x = x
|
|
|
|
cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
|
|
cong f Refl = Refl
|
|
|
|
thm : {A : U} (xs ys : List A) -> length (xs ++ ys) ≡ length xs + length ys
|
|
thm Nil ys = Refl
|
|
thm (x :: xs) ys = cong S (thm xs ys)
|