Module `Dolmen_type.Def`

Definitions as declarations

module Declare : functor (Type : Tff_intf.S) -> sig ... end: Handle definitions as declaring new constants.

Definitions using substitution

module type Subst_arg = sig ... end: Signature for substitution functions over types and terms

module Subst : functor (Type : Tff_intf.S) -> functor (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) -> sig ... end: Handle definitions by subsituting in the bodies during type-checking.