		Search-engine friendly clone of the ACL2 documentation.

Atc-var-info

Make-atc-var-info

Basic constructor macro for atc-var-info structures.

Syntax

(make-atc-var-info [:type <type>] 
                   [:thm <thm>] 
                   [:externalp <externalp>])

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

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

Definition

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

Macro: make-atc-var-info

(defmacro make-atc-var-info (&rest args)
  (std::make-aggregate 'atc-var-info
                       args '((:type) (:thm) (:externalp))
                       'make-atc-var-info
                       nil))

Function: atc-var-info

(defun atc-var-info (type thm externalp)
  (declare (xargs :guard (and (typep type)
                              (symbolp thm)
                              (booleanp externalp))))
  (declare (xargs :guard t))
  (let ((__function__ 'atc-var-info))
    (declare (ignorable __function__))
    (b* ((type (mbe :logic (type-fix type) :exec type))
         (thm (mbe :logic (symbol-fix thm) :exec thm))
         (externalp (mbe :logic (acl2::bool-fix externalp)
                         :exec externalp)))
      (list (cons 'type type)
            (cons 'thm thm)
            (cons 'externalp externalp)))))