|
|
|---|
|
|
|
|---|
Fixtype of validation information for integer constants.
This is a product type introduced by fty::defprod.
This is the type of the annotations that the validator adds to integer constants, i.e. the iconst constructs. The information consists of the type of the constant (which for now we do not constrain to be an integer type), and the numeric value of the constant, as an ACL2 natural number.