		Search-engine friendly clone of the ACL2 documentation.

Te-args

Make-te-args

Basic constructor macro for te-args structures.

Syntax

(make-te-args [:expr-lst <expr-lst>] 
              [:fn-lst <fn-lst>] 
              [:fty-info <fty-info>] 
              [:symbol-index <symbol-index>] 
              [:symbol-list <symbol-list>] 
              [:avoid-list <avoid-list>] 
              [:symbol-map <symbol-map>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-te-args

(defmacro make-te-args (&rest args)
  (std::make-aggregate 'te-args
                       args
                       '((:expr-lst)
                         (:fn-lst)
                         (:fty-info)
                         (:symbol-index)
                         (:symbol-list)
                         (:avoid-list)
                         (:symbol-map))
                       'make-te-args
                       nil))

Function: te-args

(defun te-args (expr-lst fn-lst fty-info symbol-index
                         symbol-list avoid-list symbol-map)
 (declare (xargs :guard (and (pseudo-term-listp expr-lst)
                             (func-alistp fn-lst)
                             (fty-info-alist-p fty-info)
                             (natp symbol-index)
                             (string-listp symbol-list)
                             (symbol-listp avoid-list)
                             (symbol-string-alistp symbol-map))))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'te-args))
   (declare (ignorable acl2::__function__))
   (b* ((expr-lst (mbe :logic (pseudo-term-list-fix expr-lst)
                       :exec expr-lst))
        (fn-lst (mbe :logic (func-alist-fix fn-lst)
                     :exec fn-lst))
        (fty-info (mbe :logic (fty-info-alist-fix fty-info)
                       :exec fty-info))
        (symbol-index (mbe :logic (nfix symbol-index)
                           :exec symbol-index))
        (symbol-list (mbe :logic (str::string-list-fix symbol-list)
                          :exec symbol-list))
        (avoid-list (mbe :logic (symbol-list-fix avoid-list)
                         :exec avoid-list))
        (symbol-map (mbe :logic (symbol-string-alist-fix symbol-map)
                         :exec symbol-map)))
     (list (cons 'expr-lst expr-lst)
           (cons 'fn-lst fn-lst)
           (cons 'fty-info fty-info)
           (cons 'symbol-index symbol-index)
           (cons 'symbol-list symbol-list)
           (cons 'avoid-list avoid-list)
           (cons 'symbol-map symbol-map)))))