package dolmen_type

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Floating points are complicated so this documentation is not in anyway sufficient. A detailed description of the theory together with the rationale of several models decisions as well as a formal semantics of the theory can be found in

BTRW15 Martin Brain, Cesare Tinelli, Philipp Ruemmer, and Thomas Wahl. An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic Technical Report, 2015. (http://smt-lib.org/papers/BTRW15.pdf)

val ty : Type.T.t -> Type.Ty.t

Type of a term.

Sub-module used for namespacing the real part of the theory requirements

Sub-module used for namespacing the bitvector part of the theory requirements

Sub-module used for namespacing the floating number part of the theory requirements