term-rewriting-0.3.0.1: Term Rewriting Library
Data.Rewriting.Substitution.Match
match :: (Eq f, Ord v, Eq v') => Term f v -> Term f v' -> Maybe (GSubst v f v') Source #
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