[Agda] Bug in record definition

[Nicolas Pouillard]

On Mon, 28 Mar 2011 15:41:45 +0200, Nils Anders Danielsson <nad at chalmers.se> wrote:
> On 2011-03-28 12:58, Nicolas Pouillard wrote:
> > I would be in favor of this change to. At least by a flag to begin with.
> > Does anybody want to keep this feature and why?
> 
> I have used this feature. Example:
> 
>    ^-initial : ∀ {R} → List R → (n : ℕ) → List (Vec R n)
>    ^-initial _ zero    = _
>    ^-initial _ (suc _) = _
> 
>    _^_ : ∀ {Tok R xs} →
>          Parser Tok R xs → (n : ℕ) → Parser Tok (Vec R n) (^-initial xs n)
>    p ^ 0     = return []
>    p ^ suc n = _∷_ <$> p ⊛ p ^ n
> 
> Here the body of _^_ determines the body of ^-initial. However, I would
> not mind putting these definitions in a mutual block.

Actually I was expecting you to show some examples :)
And I agree that allowing "mutual" here would be a fine compromise.

-- 
Nicolas Pouillard
http://nicolaspouillard.fr