Module Theory.Float

Sorts for floating-point numbers.

module Format : sig ... end

Sort describing the representation format of a floating-point number.

type ('r, 's) format = ('r, 's) Format.t
type 'f t
val define : ('r, 's) format Value.sort -> ('r, 's) format t Value.sort

define r s defines a floating-point sort, indexed by the floating-point format r that gives the interpretation to the bits of bitvectors of sort s.

val refine : unit Value.sort -> ('r, 's) format t Value.sort option

refine s if s is a floating-point sort then restores its type.

val format : ('r, 's) format t Value.sort -> ('r, 's) format Value.sort

format s returns the format of floating-points of sort s.

val bits : ('r, 's) format t Value.sort -> 's Bitv.t Value.sort

bits s returns the sort of bitvectors that are used to represent floating-point numbers of sort s.