		Search-engine friendly clone of the ACL2 documentation.

G-boolean

Make-g-boolean

Basic constructor macro for g-boolean structures.

Syntax

(make-g-boolean [:bool <bool>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-g-boolean

(defmacro make-g-boolean (&rest args)
  (std::make-aggregate 'g-boolean
                       args '((:bool))
                       'make-g-boolean
                       nil))

Function: g-boolean

(defun g-boolean (bool)
  (declare (xargs :guard t))
  (let ((__function__ 'g-boolean))
    (declare (ignorable __function__))
    (cons :g-boolean bool)))