[Agda] Mixfix binders: first patch

[Jean-Philippe Bernardy]

On Mon, Sep 13, 2010 at 2:08 AM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
> On 2010-09-12 11:45, Jean-Philippe Bernardy wrote:
>>
>> I have implemented a bit more of this, and uploaded the patch bundle
>> to the issue tracker.

> * One cannot use implicit arguments on the left-hand side of a syntax
>  declaration:
>
>    id : {A : Set} → A → A
>    id x = x
>
>    syntax id {A} x = x ∶ A  -- Parse error.
>
>  Is this intentional?

Yes, I would like at least to stabilize the current code before "going crazy" :)

> * I have reported some bugs related to your patches:
>
>    http://code.google.com/p/agda/issues/detail?id=307
>    http://code.google.com/p/agda/issues/detail?id=308
>    http://code.google.com/p/agda/issues/detail?id=309

I have submitted patches to 307 that fixes some of these.

Thanks for the review and the reports!

Cheers,
JP.