[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