[Agda] Fwd: Coinductive datatypes

[Ulf Norell]

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

> Hi,
>
> I've misunderstood some concepts.
>
> What I was meaning is how to construct an inductive-recursive data type in
> agda. Forget about coinduction and the codata keyword.
>
> Is there a way to implement the inductive-recursive DList datatype in
> Agda2? Is there a way to avoid scope checking errors in the following
> program?
>

You need to put both definitions in a mutual block

mutual

  data DList : Set where
    nil : DList
    cons : (a : Nat) -> (l : DList) -> {_ : True (Fresh a l)} -> DList

  Fresh : (a : Nat) -> (DList) -> Bool
  Fresh a nil = t
  Fresh a (cons b bs) = if (a # b) then (Fresh a bs) else f

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