package dolmen

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

The type of statements.

val logic : ?loc:L.t -> ac:bool -> I.t list -> T.t -> t

Function declaration.

val record_type : ?loc:L.t -> I.t -> T.t list -> (I.t * T.t) list -> t

Record type definition.

val fun_def : ?loc:L.t -> I.t -> T.t list -> T.t list -> T.t -> T.t -> t

Function definition.

val pred_def : ?loc:L.t -> I.t -> T.t list -> T.t list -> T.t -> t

Predicate definition.

val abstract_type : ?loc:L.t -> I.t -> T.t list -> t

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

val algebraic_type : ?loc:L.t -> I.t -> T.t list -> (I.t * T.t list) list -> t

An algebraic datatype definition.

val rec_types : ?loc:L.t -> t list -> t

Pack a list of mutually recursive algebraic datatypes together.

val axiom : ?loc:L.t -> I.t -> T.t -> t

Create an axiom.

val case_split : ?loc:L.t -> I.t -> T.t -> t

Create a case split.

val theory : ?loc:L.t -> I.t -> I.t -> t list -> t

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

val rewriting : ?loc:L.t -> I.t -> T.t list -> t

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

val prove_goal : ?loc:L.t -> I.t -> T.t -> t

Goal declaration.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct