[Agda] Instance arguments: three more updates

Dominique Devriese dominique.devriese at cs.kuleuven.be
Thu May 5 13:51:19 CEST 2011


All,

I've implemented three more changes related to recently added
"instance arguments". I consider these changes ready for inclusion.

* Name change "non-canonical implicit arguments" to "instance
arguments (thanks to Andreas for the suggestion): name changed
throughout source code and documentation. The code also still
contained references to an older name "ImplicitFromScope", which I
changed to "Instance" as well.

* Add support for instance arguments in the reflection API: this was
still missing. It was very easy to do thanks to the changes in
Nicolas' recently merged patch " Extend the reflection API"

* Introduce a cleaner and more efficient replacement for the
RecordWithImplicits macro's. The new syntax is
     module RecordWithImplicits = Record {{...}}
  and
     open Record {{...}}
  and variations with "open module ...", "open ... public" and
using/renaming/hiding stuff

  This could also allowed me to simplify the code a bit, by
generalising normal ModuleMacro's and removing pre-existing
duplication in the code between LetApply and Apply.

The changes can be pulled from the following darcs repository:
  http://people.cs.kuleuven.be/dominique.devriese/Agda-ncia-trunk

(should be up to date with latest upstream)

Any comments?  Okay for inclusion?

Dominique


More information about the Agda mailing list