dolmen_type

A typechecker for automated deduction languages
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen_type
Module Dolmen_type . Def . Subst

Parameters

module Type : Tff_intf.S
module T : Subst_arg with type ty := Type.Ty.t and type ty_var := Type.Ty.Var.t and type term := Type.T.t and type term_var := Type.T.Var.t

Signature

val define_ty : Type.env -> Dolmen.Std.Id.t -> Type.Ty.Var.t list -> Type.Ty.t -> unit

Define a type constant.

val define_term : Type.env -> Dolmen.Std.Id.t -> Type.Ty.Var.t list -> Type.T.Var.t list -> Type.T.t -> unit

Define a term constant.

Adequate builtin symbols function for constants defined/declared.