3 ms·
Interesting to see you can jam something like this into Haskell despite its inappropriateness. The (genuine) Agda proofs are much, much nicer.
by tel 12y ago
Interesting to see you can jam something like this into Haskell despite its inappropriateness. The (genuine) Agda proofs are much, much nicer.
- cousin_it 12y agoAgreed :-) 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.