1signature FullUnify =
2sig
3
4  type hol_type = Type.hol_type
5  type term = Term.term
6  type ('a,'b) subst = ('a,'b)Lib.subst
7  structure Env : sig
8     type t
9     type 'a EM = (t,'a) optmonad.optmonad
10     val empty : t
11     val add_tybind : string * hol_type -> unit EM
12     val add_tmbind : term * term -> unit EM
13     val lookup_ty : t -> hol_type -> hol_type
14     val lookup_tm : t -> term -> term
15     val instE : t -> term -> term
16     val triTM : t -> (term,term)Binarymap.dict
17     val triTY : t -> (string,hol_type)Binarymap.dict
18     val fromEmpty : 'a EM -> 'a option
19  end
20
21  val unify_types : hol_type list -> hol_type * hol_type -> unit Env.EM
22  val unify : hol_type list -> term list -> term * term -> unit Env.EM
23  val collapse : ((hol_type,hol_type)subst * (term,term) subst) Env.EM
24
25end
26