[Agda] Mixfix binders: first patch

[Nils Anders Danielsson]

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.

Thanks!

You wanted us to discuss the internals of Agda on the mailing list. Here
goes:

* Whenever you change the interface file format you should update
   Agda.TypeChecking.Serialise.currentInterfaceVersion.

* When a new feature is implemented it should be documented in
   doc/release-notes/<next-version>.txt. It is also a good idea to add
   test cases under test/succeed and test/fail, and maybe also
   test/interaction.

* Please use __IMPOSSIBLE__ instead of calls to error. __IMPOSSIBLE__
   generates errors of the following form:

     An internal error has occurred. Please report this as a bug.
     Location of the error: ...

   Calls to error can make Agda fail with an error message in the *ghci*
   buffer.

* You had a question about UseBoundNames/DontUseBoundNames. These
   constructors are documented in Agda.Syntax.Concrete.Operators.

* 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?

* 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

--
/NAD