package dolmen

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

Signature required by types for typing smtlib bitvectors

type t

The type of types

val bitv : int -> t

Create a fixed size bitvector type.

type view = private [>
  1. | `Bitv of int
]

Partial views for types. These are used in the bitv theory to check invariant on indexes of bitv operations (e.g. check that the indexes of an extract do not go out of bounds).

val view : t -> view

Partial view of a type.

OCaml

Innovation. Community. Security.