<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">https://www.youtube.com/watch?v=8WFMK0hv8bE</a> <br></div>