[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

The following Agda code is related:

http://www.cs.bham.ac.uk/~mhe/pigeon/

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

Martin

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