		Search-engine friendly clone of the ACL2 documentation.

G-concrete

Make-g-concrete

Basic constructor macro for g-concrete structures.

Syntax

(make-g-concrete [:val <val>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-g-concrete

(defmacro make-g-concrete (&rest args)
  (std::make-aggregate 'g-concrete
                       args '((:val))
                       'make-g-concrete
                       nil))

Function: g-concrete

(defun g-concrete (val)
  (declare (xargs :guard t))
  (let ((__function__ 'g-concrete))
    (declare (ignorable __function__))
    (if (and (atom val)
             (not (and (symbolp val)
                       (member-eq val (fgl-object-keys)))))
        val
      (cons :g-concrete val))))