[Agda] Quotient types in Agda, if you Trust Me

[Matteo Acerbi]

On Wed, May 13, 2015 at 5:16 PM, Dan Licata <drl at cs.cmu.edu> wrote:
> Hi Matteo,
>
> Oops, the second datatype and the #out and #in functions were supposed to be indented into the private block, but they weren't.  I think the updated version on github prevents this problem?

It does. I had not noticed that in quotient.agda more definitions were
private. :-)

Now I guess I understand the trick, nice!

> Assuming the injectivity/disjointness analyses could be disabled, how would your proposal for private pattern matching be different than a private datatype?

If this approach is and will remain safe, maybe my proposal is not
worth implementing.

I'm curious to make some experiments with quotient.agda, thanks for
providing this encoding!

Best,
Matteo