[Agda] Re: Classical Mathematics for a Constructive World

Jan Burse janburse at fastmail.fm
Mon Nov 26 22:03:27 CET 2012

Jan Burse schrieb:
> It can be used in connection with some double negation
> translation (DNT) to show the corrolar that an intuitionistic
> consequence is also a classical consequence.

I don't mean Glivenko's theorem itself by the above.

More information about the Agda mailing list