logic-classes-1.4.8: 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