[Agda] `syntax'

[Nils Anders Danielsson]

On 2012-10-15 18:52, Daniel Peebles wrote:
> No, but those local let opens people were talking about recently can.
> Another option that I use sometimes is to make a local "dummy" module
> parametrized by the DTO, open the DTO, and then define your record
> inside it:
>
> module Dummy {c l1 l2: Level} (ord : DTO c l1 l2) where
>    open DTO ord
>    record Merge1 (m : Carrier) (xs: List Carrier) (ys : List Carrier) : Set where
>      ...
>
> open Dummy

I sometimes use the following construction:

   private

     module Dummy ... where
       ...

   open Dummy public

I've considered adding some kind of short-hand syntax for it.

-- 
/NAD