package dolmen

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Builtin : sig ... end

This module defines the builtins that are defined by Dolmen.

module Escape : sig ... end

Escaping identifiers

module Expr : sig ... end
module Id : sig ... end

Standard implementation of identifiers

module Loc : sig ... end

Standard implementation of file locations.

module Misc : sig ... end
module Msg : sig ... end
module Normalize : sig ... end

Normalizing functions

module Pretty : sig ... end

Pretty printing annotations

module Statement : sig ... end

Standard imlplementation of statements. This module provides a reasonable and standard implementation of statements, that can directly be used to instantiated the various functors of the dolmen library. These statements are closer to smtlib statements than to other languages statements because it is easier to express other languages statements using smtlib's than the other way around. Still, a generalisation of smtlib statements was needed so as not to lose some important distinctions between conjectures and assertions for instance.

module Tag : sig ... end

Tags

module Term : sig ... end

Standard implementation of terms

module Tok : sig ... end
module Transformer : sig ... end
module Vec : sig ... end

Resieable arrays

OCaml

Innovation. Community. Security.