[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.

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



More information about the Agda mailing list