dolmen

A parser library for automated deduction
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen.intf
Module Dolmen_intf . Term . Tff . Cstr
type t

An algebraic type constructor. Note that such constructors are used to build terms, and not types, e.g. consider the following: type 'a list = Nil | Cons of 'a * 'a t, then Nil and Cons are the constructors, while list would be a type constant of arity 1 used to name the type.

val compare : t -> t -> int

Comparison function on constant symbols.

val arity : t -> int * int

Returns the arity of a constructor.

val pattern_arity : t -> ty -> ty list -> ty list

Used in the type-checking of pattern matching. pattern_arity cstr ret ty_args should return the types of the expected arguments args such that apply_cstr cstr ty_args args has type ret.