[Agda] Instance arguments: three more updates

[Dominique Devriese]

Nils,

2011/5/5 Nils Anders Danielsson <nad at chalmers.se>:
> 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?

Yes, they are. An example (adapted from
examples/instance-arguments/02-classes-indep.agda):

  record Monoid (t : Set) : Set where
    field
      zeroT : t
      plusT : t → t → t

  mBool : Monoid Bool
  mBool = record { zeroT = false; plusT = or }

  open Monoid {{...}}

  test4 : Bool
  test4 = zeroT

This works well in the parser, because the three dots syntax "..." is
reserved (for with patterns), but was previously not legal in this
context. I personally like the syntax, but I don't have strong
feelings about it if opinions differ. Alternative suggestions are of
course welcome.

Dominique