		Search-engine friendly clone of the ACL2 documentation.

Fhg-args

Make-fhg-args

Basic constructor macro for fhg-args structures.

Syntax

(make-fhg-args [:term-lst <term-lst>] 
               [:fn-lst <fn-lst>] 
               [: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-args structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-fhg-args

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

Function: fhg-args

(defun fhg-args (term-lst fn-lst fn-returns-hint-acc
                          fn-more-returns-hint-acc lambda-acc)
 (declare
      (xargs :guard (and (pseudo-term-listp term-lst)
                         (func-alistp fn-lst)
                         (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-args))
   (declare (ignorable acl2::__function__))
   (b*
     ((term-lst (mbe :logic (pseudo-term-list-fix term-lst)
                     :exec term-lst))
      (fn-lst (mbe :logic (func-alist-fix fn-lst)
                   :exec fn-lst))
      (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 'term-lst term-lst)
           (cons 'fn-lst fn-lst)
           (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)))))