[Agda] Re: A Demonstration of Agda by Alan Jeffrey

[mukesh tiwari]

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


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


/Users/mukeshtiwari/Programming/Code/Agda/AgdaDemo.agda:68,24-41
.n != suc 0 of type ℕ
when checking that the expression x ::: xs +++ ys has type
List# .A ((.n₁ ⊹ 1) ⊹ .n)

Regards
Mukesh Tiwari



On Sun, Mar 24, 2013 at 3:12 AM, mukesh tiwari <mukeshtiwari.iiitm at gmail.com
> wrote:

> 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/33e3caa3/attachment.html