[Agda] A Demonstration of Agda by Alan Jeffrey

[Guillaume Brunerie]

Try with C-c C-Space instead.
I think the name of some commands changed at some point and now
"refine" does something completely different.

Guillaume

2013/3/23 mukesh tiwari <mukeshtiwari.iiitm at gmail.com>:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>