対話的定理証明器という言葉を見かけました j-bobに1行足しては結果を見てまた1行足す、ってやってるのを思い出して ああこれは対話してたんだ、と思うなど さて (defun list0? (x) (equal x '())) (defun list1? (x) (if (atom x) 'nil (list0? (cdr x)))) …