定理証明手習い (67) J-Bob/何
ひとことでどういうグループかは言い難い
(if-QAE e)
if型からQ、A、Eのリストを作る
(QAE-if e)
Q、A、Eのリストからif型を作る
こうやっても書けるけどlist3
と`if-c
で作ってる
その方がスジがいいんだろうか
(defun if-QAE (es) (untag es))
(defun QAE-if (es) (tag 'if es))
こうは書けないんだな
(defun if-QAE untag)
これなら通るけどJ-Bob的には非合法だろう
(define if-QAE untag)
ratorって何
(defun rator? (name)
(member? name '(equal atom car cdr cons natp size + <)))
何かの略?
組み込み関数ってなんだっけ built-in function かな?
ぜんぜん違うな
こういう関数だと、'equal
や'atom
なら't
を返すのは当然として
それ以外のときには絶対に'nil
を返すってことを言わなきゃだな
どう書けばいいかな
こんな感じか('equal
と'atom
以外は省略)
(dethm rator?/nil (x)
(if (equal x 'equal)
't
(if (equal x 'atom)
't
(equal (rator? x) 'nil))))
rator?
組み込み関数かどうか
rator.formals
組み込み関数の仮引数のリスト
def.name
defun型またはdethm型のname
def.formals
defun型またはdethm型のformals
どうもこのへん、関数がどういう考え方でグループに分けられているのかよくわからない
後方参照ができない、ってのはあるとして
defun、dethmグループとifグループとかに分けられそうな気はするんだけど