4 ms·
Proving Cantor's Theorem in Clojure Using LaTTe
- zampino 8y agoThis was my very first experiment with LaTTe (https://github.com/latte-central/LaTTe https://github.com/latte-central/LaTTe) and with proof assistants in general. You can remix the short article in nextjournal (using the invite code curryon2018) to start playing around with LaTTe proofs. This is also a nice explanation of the lambda calculus involved https://latte-central.github.io/LaTTe/102_Lambda_the_ultimate.html https://latte-central.github.io/LaTTe/102_Lambda_the_ultimat..., still I couldn't find exactly how LaTTe relates to the (I assume) more popular Coq, except both being based on the calculus of constructions. Anyone with some insights?
- zampino 8y agoYou can sign up for a nextjournal account using the invite code curryon2018 and remix the article.