		Search-engine friendly clone of the ACL2 documentation.

Fgl-object

G-concrete

FGL-object constructor for constant (quoted) objects.

This is a product type, introduced by defflexsum in support of fgl-object.

Fields

val

An object constructed as (g-concrete val) evaluates to val. Atoms other than the FGL object keywords (listed below) are represented as themselves. Other objects are represented as (:g-concrete . obj).

The FGL object keywords are members of the list (fgl-object-keys), namely:

(:g-concrete :g-boolean :g-integer
             :g-ite :g-apply
             :g-var :g-map)

All atoms other than these are FGL objects representing themselves.

Subtopics

Make-g-concrete: Basic constructor macro for g-concrete structures.
G-concrete->val: Get the val field from a g-concrete.
Change-g-concrete: Modifying constructor for g-concrete structures.