9 lines
304 B
OCaml
9 lines
304 B
OCaml
(*
|
|
The function `unify` must compute the substitution
|
|
`s` such that if `unify t1 t2 = Some s` then
|
|
`apply s t1 = apply s t2`.
|
|
|
|
You can use the slides on the Herbrand / Robinson algorithm
|
|
to start designing your implementation.
|
|
*)
|
|
val unify : Type.t -> Type.t -> TypeSubstitution.t option
|