		Search-engine friendly clone of the ACL2 documentation.

Fhg-single-args

Make-fhg-single-args

Basic constructor macro for fhg-single-args structures.

Syntax

(make-fhg-single-args [:fn <fn>] 
                      [:actuals <actuals>] 
                      [:fn-returns-hint-acc <fn-returns-hint-acc>] 
                      [:fn-more-returns-hint-acc <fn-more-returns-hint-acc>] 
                      [:lambda-acc <lambda-acc>])

This is the usual way to construct fhg-single-args structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-fhg-single-args

(defmacro make-fhg-single-args (&rest args)
  (std::make-aggregate 'fhg-single-args
                       args
                       '((:fn)
                         (:actuals)
                         (:fn-returns-hint-acc)
                         (:fn-more-returns-hint-acc)
                         (:lambda-acc))
                       'make-fhg-single-args
                       nil))

Function: fhg-single-args

(defun fhg-single-args (fn actuals fn-returns-hint-acc
                           fn-more-returns-hint-acc lambda-acc)
 (declare
      (xargs :guard (and (func-p fn)
                         (pseudo-term-listp actuals)
                         (hint-pair-listp fn-returns-hint-acc)
                         (hint-pair-listp fn-more-returns-hint-acc)
                         (lambda-binding-listp lambda-acc))))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'fhg-single-args))
   (declare (ignorable acl2::__function__))
   (b*
     ((fn (mbe :logic (func-fix fn) :exec fn))
      (actuals (mbe :logic (pseudo-term-list-fix actuals)
                    :exec actuals))
      (fn-returns-hint-acc
           (mbe :logic (hint-pair-list-fix fn-returns-hint-acc)
                :exec fn-returns-hint-acc))
      (fn-more-returns-hint-acc
           (mbe :logic (hint-pair-list-fix fn-more-returns-hint-acc)
                :exec fn-more-returns-hint-acc))
      (lambda-acc (mbe :logic (lambda-binding-list-fix lambda-acc)
                       :exec lambda-acc)))
     (list (cons 'fn fn)
           (cons 'actuals actuals)
           (cons 'fn-returns-hint-acc
                 fn-returns-hint-acc)
           (cons 'fn-more-returns-hint-acc
                 fn-more-returns-hint-acc)
           (cons 'lambda-acc lambda-acc)))))