package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

Implementation requirement for the TPTP 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 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.