[Agda] `syntax'

Nils Anders Danielsson nad at chalmers.se
Mon Oct 15 19:55:33 CEST 2012

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:


     module Dummy ... where

   open Dummy public

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


More information about the Agda mailing list