Parameter Make.S

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.