[Agda] A Demonstration of Agda by Alan Jeffrey

[mukesh tiwari]

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".

module AgdaDemo where

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

[1] https://www.youtube.com/watch?v=8WFMK0hv8bE
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130324/12a26533/attachment.html