		Search-engine friendly clone of the ACL2 documentation.

Structdeclor

Make-structdeclor

Basic constructor macro for structdeclor structures.

Syntax

(make-structdeclor [:declor? <declor?>] 
                   [:expr? <expr?>])

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

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

Definition

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

Macro: make-structdeclor

(defmacro make-structdeclor (&rest args)
  (std::make-aggregate 'structdeclor
                       args '((:declor?) (:expr?))
                       'make-structdeclor
                       nil))

Function: structdeclor

(defun structdeclor (declor? expr?)
  (declare (xargs :guard (and (declor-optionp declor?)
                              (const-expr-optionp expr?))))
  (declare (xargs :guard t))
  (let ((__function__ 'structdeclor))
    (declare (ignorable __function__))
    (b* ((declor? (mbe :logic (declor-option-fix declor?)
                       :exec declor?))
         (expr? (mbe :logic (const-expr-option-fix expr?)
                     :exec expr?)))
      (list (cons 'declor? declor?)
            (cons 'expr? expr?)))))