		Search-engine friendly clone of the ACL2 documentation.

Input-item

Make-input-item

Basic constructor macro for input-item structures.

Syntax

(make-input-item [:name <name>] 
                 [:type <type>] 
                 [:value <value>])

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

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

Definition

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

Macro: make-input-item

(defmacro make-input-item (&rest args)
  (std::make-aggregate 'input-item
                       args '((:name) (:type) (:value))
                       'make-input-item
                       nil))

Function: input-item

(defun input-item (name type value)
  (declare (xargs :guard (and (identifierp name)
                              (input-typep type)
                              (input-expressionp value))))
  (declare (xargs :guard t))
  (let ((__function__ 'input-item))
    (declare (ignorable __function__))
    (b* ((name (mbe :logic (identifier-fix name)
                    :exec name))
         (type (mbe :logic (input-type-fix type)
                    :exec type))
         (value (mbe :logic (input-expression-fix value)
                     :exec value)))
      (cons :input-item (list (cons 'name name)
                              (cons 'type type)
                              (cons 'value value))))))