[Agda] A question of terminology

[Thorsten Altenkirch]

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

I thought this was a nice feature, maybe it can be switched on via a pragma?

Thorsten