Re:A proof of Löb's theorem in Haskell
by cousin_it on Saturday September 20, 2014 @12:49PM
(#8344918)
Agreed :-)
One of the big questions to me now is whether we can prove the Diagonal Lemma, not just assume it. Do you know if it's possible in Agda? I heard somewhere that it might be hard to find an intuitionistic proof.
One of the big questions to me now is whether we can prove the Diagonal Lemma, not just assume it. Do you know if it's possible in Agda? I heard somewhere that it might be hard to find an intuitionistic proof.