Basic constructor macro for lambda-binding structures.
(make-lambda-binding [:formals <formals>] [:actuals <actuals>])
This is the usual way to construct lambda-binding structures. It simply conses together a structure with the specified fields.
This macro generates a new lambda-binding structure from scratch. See also change-lambda-binding, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-lambda-binding (&rest args) (std::make-aggregate 'lambda-binding args '((:formals) (:actuals)) 'make-lambda-binding nil))
Function:
(defun lambda-binding (formals actuals) (declare (xargs :guard (and (symbol-listp formals) (pseudo-term-listp actuals)))) (declare (xargs :guard (equal (len formals) (len actuals)))) (let ((acl2::__function__ 'lambda-binding)) (declare (ignorable acl2::__function__)) (b* ((formals (mbe :logic (symbol-list-fix formals) :exec formals)) (actuals (mbe :logic (pseudo-term-list-fix actuals) :exec actuals))) (let ((formals (mbe :logic (lambda->formals-fix formals actuals) :exec formals)) (actuals (mbe :logic (lambda->actuals-fix formals actuals) :exec actuals))) (list (cons 'formals formals) (cons 'actuals actuals))))))