[Agda] Postulated computing quotients are unsound

Nils Anders Danielsson nad at chalmers.se
Wed May 16 16:15:12 CEST 2012

On 2012-05-16 15:50, Altenkirch Thorsten wrote:
> How can this be fixed? Can we hide things better?

I don't think we should let hacks like this influence the language
design too much.


More information about the Agda mailing list