[Agda] no-eta-equality

[Ulf Norell]

On Thu, Sep 29, 2016 at 2:16 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> You can write eDSet and eUpDSet using copatterns as follows:
>
> eDSet : DSet eDecSetoid
> dSet1 eDSet = f
>     where
>         f : eC → eC
>         f = id
>  dSet2 eDSet = g
>     where
>         g : eC → ℕ
>         g _ = 0
>
> eUpDSet : UpDSet _ _
> decSetoid eUpDSet = eDecSetoid
> dSet eUpDSet = eDSet
>

A nice thing with copatterns is that it lets you do further pattern
matching, so in this example (which doesn't use pattern matching, but it
could) you can write (patching Jespers code a little to make it check)

  eDSet : DSet eDecSetoid
  DSet.dSet1 eDSet = id
  DSet.dset2 eDSet _ = 0

  eUpDSet : UpDSet _ _
  UpDSet.decSetoid eUpDSet = eDecSetoid
  UpDSet.dSet      eUpDSet = eDSet    -- (2)


Also you shouldn't need --copatterns, they are on by default.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160929/c9c76fe3/attachment.html