		Search-engine friendly clone of the ACL2 documentation.

Let-binding

Make-let-binding

Basic constructor macro for let-binding structures.

Syntax

(make-let-binding [:bindings <bindings>] 
                  [:hypotheses <hypotheses>])

This is the usual way to construct let-binding structures. It simply conses together a structure with the specified fields.

This macro generates a new let-binding structure from scratch. See also change-let-binding, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-let-binding

(defmacro make-let-binding (&rest args)
  (std::make-aggregate 'let-binding
                       args '((:bindings) (:hypotheses))
                       'make-let-binding
                       nil))

Function: let-binding

(defun let-binding (bindings hypotheses)
  (declare (xargs :guard (and (binding-listp bindings)
                              (hint-pair-listp hypotheses))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'let-binding))
    (declare (ignorable acl2::__function__))
    (b* ((bindings (mbe :logic (binding-list-fix bindings)
                        :exec bindings))
         (hypotheses (mbe :logic (hint-pair-list-fix hypotheses)
                          :exec hypotheses)))
      (list (cons 'bindings bindings)
            (cons 'hypotheses hypotheses)))))