[Agda] Bug in record definition

[Nils Anders Danielsson]

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.

-- 
/NAD