package dolmen

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

Implementation requirement for the native alt-ergo's format.

type t

The type of statements.

type id

The type of identifiers

type term

The type of terms used in statements.

type location

The type of locations attached to statements.

val logic : ?loc:location -> ac:bool -> id list -> term -> t

Function declaration.

val record_type : ?loc:location -> id -> term list -> (id * term) list -> t

Record type definition.

val fun_def : ?loc:location -> id -> term list -> term list -> term -> term -> t

Function definition.

val pred_def : ?loc:location -> id -> term list -> term list -> term -> t

Predicate definition.

val defs : ?loc:location -> ?attrs:term list -> t list -> t

Pack a list of mutually recursive definitions into a single statement.

val abstract_type : ?loc:location -> id -> term list -> t

Create a new abstract type, quantified over the given type variables.

val algebraic_type : ?loc:location -> id -> term list -> (id * term list) list -> t

An algebraic datatype definition.

val rec_types : ?loc:location -> t list -> t

Pack a list of mutually recursive algebraic datatypes together.

val axiom : ?loc:location -> id -> term -> t

Create an axiom.

val case_split : ?loc:location -> id -> term -> t

Create a case split.

val theory : ?loc:location -> id -> id -> t list -> t

Create a theory, extending another, with the given list of declarations.

val rewriting : ?loc:location -> id -> term list -> t

Create a (set of ?) rewriting rule(s).

val prove_goal : ?loc:location -> id -> term -> t

Goal declaration.

val prove_sat : ?loc:location -> name:id -> term list -> t

Check-sat declaration.