3 ms·
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 LC
by 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.