Floating-point specification

The operators taking a rounding mode take it first, as cvc5 does. The predicates and the conversions that read a bit pattern take none.

Predicates

Arithmetic and assembly

Indexed conversions

Constructors

The exponent and significand sizes are indices, so they are explicit Nats and fix the result's own sizes.