A typechecker for automated deduction languages
Module type
Class type
Library dolmen_type
Module Dolmen_type . Thf_intf . S . T . 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.t -> Ty.t list -> Ty.t 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.