[–] JonChesterfield 3y ago ↗ Metamath style but implemented in lisp. The idea is one can write lisp functions that define theorems, analogous to using SML to define theorems in Edinburgh LCF.
1 comment
[ 2.9 ms ] story [ 99.0 ms ] thread