定理証明手習い (66) J-Bob/データ表現

データの表現方法としては、J-Bobの実装言語の構文を反映したものを選びました。

若干混乱中
「J-Bob」と「J-Bobの実装言語」は同じもの？違うもの？
別だけど揃えた、ってことはな？
J-Bob/proveとかが定義されてるのがJ-Bobだと思うんだけど
今J-Bobを定義してる言語もJ-Bobらしいし、
J-Bob/proveの中にクォートされて出てくる言語もJ-Bob?

(defun quote-c (value)
  (tag 'quote (list1 value)))
(defun quote? (x)
  (if (tag? 'quote x) (list1? (untag x)) 'nil))
(defun quote.value (e) (elem1 (untag e)))

臆面もなくboilerplateな感じがよい（よくはない

(quote-c value) quote型の値を作る
(quote? x) quote型の値かどうか
(quote.value e) eのvalue

(if-c Q A E) if型の値を作る
(if? x) if型の値かどうか
(if.Q e) eのQ
(if.A e) eのA
(if.E e) eのE

(app-c name args) app型の値を作る
(app? x) app型の値かどうか
(app.name e) eのname
(app.args e) eのargs

quoteでもifでもなければapp、って判定してるけどdefunとかdethmとかは
区別しなくていいのかなあ

(defun-c name formals body) defun型の値を作る
(defun? x) defun型の値かどうか
(defun.name e) eのname
(defun.formals e) eのformals
(defun.body e) eのbody