		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Dec-expo

Fixtype of decimal exponents [C17:6.4.4.2] [C17:A.1.5].

This is a product type introduced by fty::defprod.

Fields

prefix — dec-expo-prefix
sign? — sign-option
digits — dec-digit-char-list

This corresponds to exponent-part in the grammar in [C17]. It consists of a prefix, an optional sign, and a list of (decimal) digits (which should be non-empty).

Subtopics

Dec-expo-fix: Fixing function for dec-expo structures.
Dec-expo-equiv: Basic equivalence relation for dec-expo structures.
Make-dec-expo: Basic constructor macro for dec-expo structures.
Dec-expo->prefix: Get the prefix field from a dec-expo.
Dec-expo->digits: Get the digits field from a dec-expo.
Change-dec-expo: Modifying constructor for dec-expo structures.
Dec-expop: Recognizer for dec-expo structures.
Dec-expo->sign?: Get the sign? field from a dec-expo.