[Agda] Coinductive datatypes

[Ulf Norell]

On Thu, Sep 25, 2008 at 11:32 AM, Álvaro García Pérez <
agarcia at babel.ls.fi.upm.es> wrote:

> Hi to everybody,
>
> codata DList : Set where
>   nil : DList
>   cons : (a : Nat) -> (l : DList) -> {True (Fresh a l)} -> DList
>
> The compiler raises:
> /home/agarcia/Escritorio/Mis documentos/2007-2008/BABEL/agda/recursive.agda:57,38-56
> {True (Fresh a l)} cannot appear by itself. It needs to be the
> argument to a function expecting an implicit argument.
> when scope checking {True (Fresh a l)}
>

The error is just a syntactic one and doesn't have anything to do with
codata. Implicit arguments always have to have a name, so to get rid of the
error simply say

  cons : (a : Nat) -> (l : DList) -> {_ : True (Fresh a l)} -> DList

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080925/844d3f98/attachment.html