		Search-engine friendly clone of the ACL2 documentation.

Atc-fn-info

Make-atc-fn-info

Basic constructor macro for atc-fn-info structures.

Syntax

(make-atc-fn-info [:out-type <out-type>] 
                  [:in-types <in-types>] 
                  [:loop? <loop?>] 
                  [:affect <affect>] 
                  [:extobjs <extobjs>] 
                  [:result-thm <result-thm>] 
                  [:correct-thm <correct-thm>] 
                  [:correct-mod-thm <correct-mod-thm>] 
                  [:measure-nat-thm <measure-nat-thm>] 
                  [:fun-env-thm <fun-env-thm>] 
                  [:limit <limit>] 
                  [:guard <guard>])

This is the usual way to construct atc-fn-info structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-atc-fn-info

(defmacro make-atc-fn-info (&rest args)
  (std::make-aggregate 'atc-fn-info
                       args
                       '((:out-type)
                         (:in-types)
                         (:loop?)
                         (:affect)
                         (:extobjs)
                         (:result-thm)
                         (:correct-thm)
                         (:correct-mod-thm)
                         (:measure-nat-thm)
                         (:fun-env-thm)
                         (:limit)
                         (:guard))
                       'make-atc-fn-info
                       nil))

Function: atc-fn-info

(defun atc-fn-info
       (out-type in-types loop? affect extobjs
                 result-thm correct-thm correct-mod-thm
                 measure-nat-thm fun-env-thm limit guard)
  (declare (xargs :guard (and (type-optionp out-type)
                              (type-listp in-types)
                              (stmt-optionp loop?)
                              (symbol-listp affect)
                              (symbol-listp extobjs)
                              (symbolp result-thm)
                              (symbolp correct-thm)
                              (symbolp correct-mod-thm)
                              (symbolp measure-nat-thm)
                              (symbolp fun-env-thm)
                              (pseudo-termp limit)
                              (symbolp guard))))
  (declare (xargs :guard t))
  (let ((__function__ 'atc-fn-info))
    (declare (ignorable __function__))
    (b* ((out-type (mbe :logic (type-option-fix out-type)
                        :exec out-type))
         (in-types (mbe :logic (type-list-fix in-types)
                        :exec in-types))
         (loop? (mbe :logic (stmt-option-fix loop?)
                     :exec loop?))
         (affect (mbe :logic (symbol-list-fix affect)
                      :exec affect))
         (extobjs (mbe :logic (symbol-list-fix extobjs)
                       :exec extobjs))
         (result-thm (mbe :logic (symbol-fix result-thm)
                          :exec result-thm))
         (correct-thm (mbe :logic (symbol-fix correct-thm)
                           :exec correct-thm))
         (correct-mod-thm (mbe :logic (symbol-fix correct-mod-thm)
                               :exec correct-mod-thm))
         (measure-nat-thm (mbe :logic (symbol-fix measure-nat-thm)
                               :exec measure-nat-thm))
         (fun-env-thm (mbe :logic (symbol-fix fun-env-thm)
                           :exec fun-env-thm))
         (limit (mbe :logic (pseudo-term-fix limit)
                     :exec limit))
         (guard (mbe :logic (symbol-fix guard)
                     :exec guard)))
      (list (cons 'out-type out-type)
            (cons 'in-types in-types)
            (cons 'loop? loop?)
            (cons 'affect affect)
            (cons 'extobjs extobjs)
            (cons 'result-thm result-thm)
            (cons 'correct-thm correct-thm)
            (cons 'correct-mod-thm correct-mod-thm)
            (cons 'measure-nat-thm measure-nat-thm)
            (cons 'fun-env-thm fun-env-thm)
            (cons 'limit limit)
            (cons 'guard guard)))))