[Agda] Tentative guidelines for working with coinductive types

[Ulf Norell]

On Thu, Jan 15, 2009 at 10:54 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk>wrote:

> I would prefer "record" to be a layout keyword, so that we could drop the
> braces and
> semicolons:
>
>  _,_ : ∀ {A B} (x : A) → B x → Σ A B
>  (x , y) = record
>    proj₁ = x
>    proj₂ = y
>   map : ∀ {A B} → (A → B) → Stream A → Stream B
>  map f xs = record
>    head = f (head xs)
>    tail = map f (tail xs)
>
> (There was some problem with this, though. Ulf knows more.)


The "record" keyword is not only used when constructing record elements, but
also when declaring record types. Making it a layout keyword would mess up
the record declaration syntax.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090116/11b4d41e/attachment.html