Pf. Too convoluted. You have to define stuff in M expressions and then map them to S expressions. And what is it that you're defining? A set of primitive functi

Pf. Too convoluted. You have to define stuff in M expressions and then map them to S expressions. And what is it that you're defining? A set of primitive functions, some of them operating on specialised data structures. Why? Here's Prolog in Prolog: prove(true). prove((L,Ls)):- prove(L) ,prove(Ls). prove(L):- clause(L,Body) ,prove(Body). clause(H:-B,B). clause((H:-),true). This is just a straight-forward implementatio of SLDNF Resolution [1]. No "primitives", no data types, no specialised data structures and no translation from Prolog to something else before looping back to Prolog. Also, rather fewer LOCs. LISP people are always bragging about their LOCs. I don't know why. __________ [1] "SLDNF" Resolution is Selective Linear Definite Resolution with Negation as Failure, officially; or, Straight-up Logical Derivations with No Fuckups Resolution, as I prefer to think of it.