package dolmen

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

Module type Dolmen_ae.StatementSource

Implementation requirement for the TPTP format.

Sourcetype t

The type of statements.

Sourcetype id

The type of identifiers

Sourcetype term

The type of terms used in statements.

Sourcetype location

The type of locations attached to statements.

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

Function declaration.

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

Record type definition.

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

Function definition.

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

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

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

An algebraic datatype definition.

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

Pack a list of mutually recursive algebraic datatypes together.

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

Create an axiom.

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

Create a case split.

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

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

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

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

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

Goal declaration.

OCaml

Innovation. Community. Security.