Bug 779 [Re: [Agda] record syntax error]

[Serge D. Mechveliani]

Finally I have got it!
For several months I could not find any real bug.
------
Sergei

On Thu, Jan 03, 2013 at 11:02:47PM +0100, Andreas Abel wrote:
> This is a bug in Agda, I filed it as issue 779.
> 

Copying from `issues': -----------------------------------
  
> Agda does not find definition clause in a record if it is a with clause
> and a field declaration follows
[..]
> http://code.google.com/p/agda/issues/detail?id=779
>
> record R : Set1 where
>  Bla : Set1
>  Bla with Set
>  ... | _ = Set
>
>  field
>    F : Set
>
> Agda reports: Missing definition for Bla