[Agda] A question of terminology

[Dominique Devriese]

2011/4/28 Andreas Abel <andreas.abel at ifi.lmu.de>:
> So I am proposing
>
>  instance arguments
>
> If no one shouts, I will adjust the terminology in the Agda release notes
> very soon.

As mentioned at some point during the AIM XIII, I agree with Andreas
(and others) that "non-canonical implicit arguments" is not an ideal
name. I like "instance arguments", so I second this proposal.

Some other updates about the "instance arguments" feature:
* Ulf recently merged my patch in the main Agda repository, so I guess
  "instance arguments" will be available in Agda 2.2.12. Some tests
  and a bugfix for an interaction with freezing meta-vars are pending.

The merged code has seen some changes for comments I got during AIM
XIII, for reference:

* The generated RecordWithImplicits modules have been removed because
  they caused a significant performance increase of type checking. The
  problem was that the modules were generated and kept in memory for
  every record in the standard library, even if they were not needed.
  As I discussed in my talk in AIM XIII, the modules can be defined
  relatively easily by the user as follows:

   module RecordWithImplicits {args : Ts} {{rec : Record Ts}} = Record rec

* "instance arguments" now behave exactly as existing implicit
  arguments in the context of pretty printing records.

* Unicode characters "WHITE CURLY BRACKET, LEFT 2983" (⦃) and "WHITE
  CURLY BRACKET, RIGHT 2984" (⦄) can now be used as single-char syntax
  for '{{' and '}}'. This uses the same lexer mechanism as "→" and
  "∀", so requires spaces around the chars (unlike the ascii syntax).
  I added \{{ and \}} in agda-input.el to make this usable in emacs.
  The chars were not previously in there, and the change does not
  break the standard library.

* Some documentation of non-canonical implicits has been added in
  doc/release-notes/2-2-12.txt and on the Agda wiki. If noone shouts,
  I will update the wiki for the new name.

Dominique