[Agda] Instance arguments: three more updates

[Nils Anders Danielsson]

On 2011-05-05 13:51, Dominique Devriese wrote:
> * 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

Are the dots part of the syntax? Can you give an example?

-- 
/NAD