3 ms·
The answer is the 4th link in the article
by sometimesijust 8y ago
The answer is the 4th link in the article
- gnulinux 8y agoThe question still stands because agda handles classical mathematics just fine too. You need to postulate lem, which blocks computation, but that is a non-issue for proof checking.