		Search-engine friendly clone of the ACL2 documentation.

Syndef::acid4

Syndef::MAKE-acid4

Basic constructor macro for acid4 structures.

Syntax

(MAKE-acid4 [:id <id>])

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

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

Definition

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

Macro: make-acid4

(defmacro syndef::|MAKE-acid4| (&rest args)
  (std::make-aggregate 'syndef::|acid4|
                       args '((:|id|))
                       'syndef::|MAKE-acid4|
                       nil))

Function: acid4

(defun syndef::|acid4| (syndef::|id|)
  (declare (xargs :guard (integerp syndef::|id|)))
  (declare (xargs :guard t))
  (let ((__function__ 'syndef::|acid4|))
    (declare (ignorable __function__))
    (b* ((syndef::|id| (mbe :logic (ifix syndef::|id|)
                            :exec syndef::|id|)))
      (cons :|acid4| (list (cons 'syndef::|id| syndef::|id|))))))