acl2 を使用して、最初の引数 (リスト) を 2 番目の引数 (別のリスト) の各要素の前に再帰的に追加する関数「ins」を作成しようとしています。
(ins (something) ( (a b c) (d e f) ...))
戻り値
( (something a b c) (something d e f) ...)
そのため、そのような関数への呼び出し
(ins '((one thing)) '( ((this is)) ((something else)) ))
私たちに与えます
'( ((one thing) (this is)) ((one thing) (something else)) ))
空かどうかをチェックして、単一の要素を含むarg2リストでのみ機能する非再帰関数を思いつきました。
(defun ins(arg1 arg2)
(if (equal arg2 nil) '() (list(append arg1 (first arg2))))
)
再帰的なものを考え出そうとすると、最初の引数が 2 番目の引数のリスト内のすべての要素に追加されます。
(defun ins (arg1 arg2)
(cond
((equal arg2 nil) '())
((not(equal arg2 nil)) (ins (list(append arg1 (first arg2))) (first(rest arg2)))
)))
しかし、何があっても常にゼロになり、その理由がわかりません。そのため、再帰呼び出しが正しいかどうかさえわかりません。自明ではない再帰をトレースするのに苦労しています。