Def (dolmen_type.Dolmen

Definitions as declarations

module Declare (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
  (Type : Tff_intf.S)
  (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.