		Search-engine friendly clone of the ACL2 documentation.

Floating-point-placeholders

Floating-point-macro-placeholders

Macros to introduce more concisely the abstract placeholders for the Java floating-point operations and conversions.

All our abstract operations and conversions are weakly constraned ACL2 functions that unconditionally return results of the appropriate types. The macros capture this boilerplate structure.

For now we only introduce abstract functions that involve the float and double value sets, not the extended-exponent value sets.

The abstract functions operate not on the tagged Java primitive values, but on their underlying (i.e. untagged) values.

Subtopics

Def-primitive-unary/binary-abs-predicate: Predicate for the result of a function introduced via def-primitive-unary-abs or def-primitive-binary-abs.
Def-primitive-unary/binary-abs-term: Term for the result of a function introduced via def-primitive-unary-abs or def-primitive-binary-abs.
Def-primitive-unary-abs: Macro to introduce an abstract placeholder for a unary operation or a conversion involving floating-point values.
Def-primitive-binary-abs: Macro to introduce an abstract placeholder for a binary operation or a conversion involving floating-point values.