Data.Rewriting.Substitution.Match

Documentation

match :: (Eq f, Ord v, Eq v') => Term f v -> Term f v' -> Maybe (GSubst v f v')

Match two terms. If matching succeeds, return the resulting subtitution. We have the following property:

 match t u == Just s   ==>   apply s t == gapply s t == u