[Agda] successor / predecessor definition rejected for a tree-based natural number type

[Andrés Sicard-Ramírez]

On 2 July 2013 11:43, Paul Tarau <paul.tarau at gmail.com> wrote:
> Not in scope:
>   x at /Users/tarau/Desktop/go/art/lit/coq/vw.agda:24,27-28
> when scope checking x
> -}
>
>   s (V E (x::xs)) =  W (s x) xs  {- agda error here, claims x not in scope -}

Replace (x::xs) by (x ∷ xs), where ∷ is the Unicode symbol used by Data.List.

-- 
Andrés