Safe Haskell | Safe-Inferred |
---|

Substitution and finding variables are two basic operations on formulas that contain terms and variables. If a formula type supports quantifiers we can also find free variables, otherwise all variables are considered free.

# Documentation

class Atom atom term v | atom -> term v whereSource

substitute :: Map v term -> atom -> atomSource

allVariables :: atom -> Set vSource

freeVariables :: atom -> Set vSource

unify :: Map v term -> atom -> atom -> Failing (Map v term)Source

match :: Map v term -> atom -> atom -> Failing (Map v term)Source

Very similar to unify, not quite sure if there is a difference

foldTerms :: (term -> r -> r) -> r -> atom -> rSource