# [Agda] A Demonstration of Agda by Alan Jeffrey

mukesh tiwari mukeshtiwari.iiitm at gmail.com
Sat Mar 23 22:42:37 CET 2013

```Hello all
I am watching this agda tutorial [1] and tried to code the concatenation of
finite list but I am getting this error "Can not refine".

data Bool : Set where
true : Bool
false : Bool

¬ : Bool → Bool
¬ true = false
¬ false = true

_^_ : Bool → Bool → Bool
true ^ y = y
false ^ y = false

data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}

_⊹_ : ℕ → ℕ → ℕ
zero ⊹ y = y
suc x ⊹ y = suc (x ⊹ y)

_==_ : ℕ → ℕ → Bool
zero == zero = true
zero == suc y = false
suc x == zero = false
suc x == suc y = x == y

infixr 5 _::_

data List ( A : Set ) : Set where
[] : List A
_::_ : A → List A → List A

_++_ : ∀ { A } → List A → List A → List A
[] ++ ys = ys
(x :: xs) ++ ys = x :: xs ++ ys

infixr 5 _:::_

data List# ( A : Set ) : ℕ → Set where
[] : List# A 0
_:::_ : ∀ { n } → A → List# A n → List# A (n ⊹ 1)

_+++_ : ∀ { A m n } → List# A m → List# A n → List# A ( m ⊹ n )
[] +++ ys = ys
(x ::: xs) +++ ys = {!x ::: ( xs +++ ys )!} -- C-c C-r gives "Can not
refine"

Could some one please tell me how to solve this problem.

Regards
Mukesh Tiwari