dolmen_type

A typechecker for automated deduction languages
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen_type
Parameter #2 Dolmen_type . Float . Smtlib2 . Tff . Ty
val bitv : int -> Type.Ty.t

Create a fixed size bitvector type.

val float : int -> int -> Type.Ty.t

Create a float type with fixed exponent size in bits and fixed significand, including the hidden bit.

val roundingMode : Type.Ty.t

Type of the rounding modes

type view#row

Partial views for types. These are used in the Float theory to perform type-base dispatch for some conversion functions.

and view = private [>
| `Real
| `Bitv of int
| `Float of int * int
]

Partial views for types. These are used in the Float theory to perform type-base dispatch for some conversion functions.

val view : Type.Ty.t -> view

Partial view of a type.