logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving
Data.Logic.Harrison.Unif
unify :: Term term v f => Map v term -> [(term, term)] -> Failing (Map v term)Source
solve :: Term term v f => Map v term -> Map v termSource
fullUnify :: Term term v f => [(term, term)] -> Failing (Map v term)Source
unifyAndApply :: Term term v f => [(term, term)] -> Failing [(term, term)]Source