dolmen_type

A typechecker for automated deduction languages
IN THIS PACKAGE
Module Dolmen_type . Def . Declare

Parameters

module Type : Tff_intf.S

Signature

val add_definition : Type.env -> Dolmen.Std.Id.t -> [ `Ty of Type.Ty.Const.t | `Term of Type.T.Const.t ] -> unit

Add a declaration binding.

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 -> Type.T.Const.t

Define a term constant.

Adequate builtin symbols function for constants defined/declared.