4 ms·
LaTTe: A Laboratory for Type Theory Experiments
- zampino 8y agoHere you have an interactive example showing how LaTTe (the lisp proof assistant written in clojure) can prove (a typed version of) Cantor Theorem on the cardinality of sets. https://news.ycombinator.com/item?id=18802480 https://news.ycombinator.com/item?id=18802480