<div dir="ltr"><div>I tried to get the more clear error message. Rather than putting holes and doing case analysis I just wrote the whole code and now this error message<br><br><br>_+++_ : ∀ { A m n } → List# A m → List# A n → List# A ( m ⊹ n )<br>
[] +++ ys = ys<br>( x ::: xs ) +++ ys =  x ::: ( xs +++ ys )<br><br><br>/Users/mukeshtiwari/Programming/Code/Agda/AgdaDemo.agda:68,24-41<br>.n != suc 0 of type ℕ<br>when checking that the expression x ::: xs +++ ys has type<br>
List# .A ((.n₁ ⊹ 1) ⊹ .n)<br><br></div>Regards <br>Mukesh Tiwari<br><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Mar 24, 2013 at 3:12 AM, mukesh tiwari <span dir="ltr">&lt;<a href="mailto:mukeshtiwari.iiitm@gmail.com" target="_blank">mukeshtiwari.iiitm@gmail.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>Hello all<br></div>I am watching this agda tutorial [1] and tried to code the concatenation of finite list but I am getting this error &quot;Can not refine&quot;. <br>
<br>module AgdaDemo where <br>
<br>data Bool : Set where <br>  true : Bool<br>  false : Bool<br><br><br>¬ : Bool → Bool<br>¬ true = false<br>¬ false = true<br><br>_^_ : Bool → Bool → Bool<br>true ^ y = y<br>false ^ y = false<br><br>data ℕ : Set where <br>

  zero : ℕ <br>  suc : ℕ → ℕ <br><br>{-# BUILTIN NATURAL ℕ #-}<br>{-# BUILTIN ZERO zero #-}<br>{-# BUILTIN SUC suc #-}<br><br><br>_⊹_ : ℕ → ℕ → ℕ <br>zero ⊹ y = y<br>suc x ⊹ y = suc (x ⊹ y)<br><br>_==_ : ℕ → ℕ → Bool<br>
zero == zero = true<br>
zero == suc y = false<br>suc x == zero = false<br>suc x == suc y = x == y <br><br>infixr 5 _::_ <br><br>data List ( A : Set ) : Set where <br>  [] : List A<br>  _::_ : A → List A → List A <br><br>_++_ : ∀ { A } → List A → List A → List A <br>

[] ++ ys = ys<br>(x :: xs) ++ ys = x :: xs ++ ys<br><br>infixr 5 _:::_ <br><br>data List# ( A : Set ) : ℕ → Set where<br>  [] : List# A 0<br>  _:::_ : ∀ { n } → A → List# A n → List# A (n ⊹ 1)<br><br><br>_+++_ : ∀ { A m n } → List# A m → List# A n → List# A ( m ⊹ n )<br>

[] +++ ys = ys<br>(x ::: xs) +++ ys = {!x ::: ( xs +++ ys )!} -- C-c C-r gives &quot;Can not refine&quot; <br><br></div><br>Could some one please tell me how to solve this problem. <br><br>Regards<br>Mukesh Tiwari<br><br>

[1] <a href="https://www.youtube.com/watch?v=8WFMK0hv8bE" target="_blank">https://www.youtube.com/watch?v=8WFMK0hv8bE</a> <br></div>
</blockquote></div><br></div>