[Agda] Postulated computing quotients are unsound

Dominique Devriese dominique.devriese at gmail.com
Wed May 16 16:27:02 CEST 2012


> * The exported constructors compute to the real ones, also in
>  equalities. For instance, [ true ] ≡ [ false ] computes to box true ≡
>  box false.

Out of interest: what would happen if [_] were made abstract?

Dominique


More information about the Agda mailing list