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.
- 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.
- Get the bits field from a g-integer.
- Basic constructor macro for g-integer structures.
- Modifying constructor for g-integer structures.