		Search-engine friendly clone of the ACL2 documentation.

Lambda-binding

Make-lambda-binding

Basic constructor macro for lambda-binding structures.

Syntax

(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.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-lambda-binding

(defmacro make-lambda-binding (&rest args)
  (std::make-aggregate 'lambda-binding
                       args '((:formals) (:actuals))
                       'make-lambda-binding
                       nil))

Function: lambda-binding

(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))))))