Module PP.Unifier

Node unifier

type unifier = node -> node -> node option

Unifier heuristic: given two nodes return None iff they don't unify, or Some x iff they unify as x

val unify : ?unify:unifier -> node list -> node list

Attempt to reduce the set of nodes by unifying multiple nodes into a single one.

  • parameter unify

    additional unifier heuristics