TPDB.DP.Unify

Documentation

mgu :: (Ord v, Eq c) => Term v c -> Term v c -> Maybe (Map v (Term v c))

naive implementation (worst case exponential)

unifies :: (Eq c, Ord v) => Term v c -> Term v c -> Bool

apply :: Ord v => Term v s -> Map v (Term v s) -> Term v s

times :: Ord v => Substitution v c -> Substitution v c -> Substitution v c