		Search-engine friendly clone of the ACL2 documentation.

Ex-args

Make-ex-args

Basic constructor macro for ex-args structures.

Syntax

(make-ex-args [:term-lst <term-lst>] 
              [:fn-lst <fn-lst>] 
              [:fn-lvls <fn-lvls>] 
              [:wrld-fn-len <wrld-fn-len>] 
              [:expand-lst <expand-lst>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-ex-args

(defmacro make-ex-args (&rest args)
  (std::make-aggregate 'ex-args
                       args
                       '((:term-lst)
                         (:fn-lst)
                         (:fn-lvls)
                         (:wrld-fn-len . 0)
                         (:expand-lst))
                       'make-ex-args
                       nil))

Function: ex-args

(defun ex-args (term-lst fn-lst fn-lvls wrld-fn-len expand-lst)
  (declare (xargs :guard (and (pseudo-term-listp term-lst)
                              (func-alistp fn-lst)
                              (sym-nat-alistp fn-lvls)
                              (natp wrld-fn-len)
                              (pseudo-term-alistp expand-lst))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'ex-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-lvls (mbe :logic (sym-nat-alist-fix fn-lvls)
                       :exec fn-lvls))
         (wrld-fn-len (mbe :logic (nfix wrld-fn-len)
                           :exec wrld-fn-len))
         (expand-lst (mbe :logic (pseudo-term-alist-fix expand-lst)
                          :exec expand-lst)))
      (list (cons 'term-lst term-lst)
            (cons 'fn-lst fn-lst)
            (cons 'fn-lvls fn-lvls)
            (cons 'wrld-fn-len wrld-fn-len)
            (cons 'expand-lst expand-lst)))))