Make.2-U
A unifier maintains a graph whose vertices are equivalence classes of variables. With each equivalence class, a piece of information of type data
is attached.
type data = variable S.structure
By definition, data
is a synonym for variable structure
. So, the data attached with an equivalence class of variables is a structure whose children are variables.