[Agda] Classical Mathematics for a Constructive World

Martin Escardo m.escardo at cs.bham.ac.uk
Mon Nov 19 14:47:23 CET 2012

The following Agda code is related:


It uses the generalized double negation monad X |-> (X->R)->R to code a 
classical proof in Agda (without postulating excluded middle).


On 19/11/12 12:44, Peter Divianszky wrote:
> Excuse me that this time I flood the mailing list with questions.
> I have read "Classical Mathematics for a Constructive World", by Russell
> O’Connor, http://arxiv.org/pdf/1008.1213
> Does someone implemented part of the paper in Agda?
> Thanks,
> Peter
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

More information about the Agda mailing list