[Agda] Record types are not allowed in mutual blocks

[Nils Anders Danielsson]

On 2011-03-18 18:15, Thorsten Altenkirch wrote:
> Is there any way to switch off this check which stops me from doing
> this?

I'm sure there is, but we want to avoid infinite η-expansion. Perhaps we
can avoid this by requiring that any cycle from a record type to itself
is "guarded" by a data type (or ∞).

-- 
/NAD