I think it is funny that the most hardcore group of FP enthusiasts seem to sympathize with constructive mathematics (e.g. proof-systems ala Coq) yet the law of the excluded middle is used in the argument here. :)
I think it is funny that the most hardcore group of FP enthusiasts seem to sympathize with constructive mathematics (e.g. proof-systems ala Coq) yet the law of the excluded middle is used in the argument here. :)