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