G-integer
FGL object constructor for symbolic integers, with Boolean functions representing the bits.
This is a product type, introduced by defflexsum in support of fgl-object.
Fields
- bits — ACL2::true-list
An object constructed as (g-integer bits) evaluates to the
two's-complement integer formed by evaluating each Boolean function
in the list bits using bfr-eval, and then converting
that Boolean list to an integer using bools->int.
Subtopics
- G-integer->bits
- Get the bits field from a g-integer.
- Make-g-integer
- Basic constructor macro for g-integer structures.
- Change-g-integer
- Modifying constructor for g-integer structures.
