logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving

Safe HaskellNone




unify_literals :: forall lit atom term v f. (Literal lit atom, Atom atom term v, Term term v f) => Map v term -> lit -> lit -> Failing (Map v term)Source

unifyAtomsEq :: forall v f atom p term. (AtomEq atom p term, Term term v f) => Map v term -> atom -> atom -> Failing (Map v term)Source

deepen :: (Int -> Failing t) -> Int -> Maybe Int -> Failing (t, Int)Source

Try f with higher and higher values of n until it succeeds, or optional maximum depth limit is exceeded.