Safe Haskell | Safe |
---|---|

Language | Haskell98 |

## Synopsis

- apply :: Ord v => Subst f v -> Term f v -> Term f v
- applyRule :: Ord v => Subst f v -> Rule f v -> Rule f v
- applyCtxt :: Ord v => Subst f v -> Ctxt f v -> Ctxt f v
- gApply :: Ord v => GSubst v f v' -> Term f v -> Maybe (Term f v')
- compose :: Ord v => Subst f v -> Subst f v -> Subst f v
- merge :: (Ord v, Eq f, Eq v') => GSubst v f v' -> GSubst v f v' -> Maybe (GSubst v f v')

# Documentation

apply :: Ord v => Subst f v -> Term f v -> Term f v Source #

Apply a substitution, assuming that it's the identity on variables not mentionend in the substitution.

applyRule :: Ord v => Subst f v -> Rule f v -> Rule f v Source #

Liftting of `apply`

to rules: applies the given substitution to left- and right-hand side.

gApply :: Ord v => GSubst v f v' -> Term f v -> Maybe (Term f v') Source #

Apply a substitution, assuming that it's total. If the term contains
a variable not defined by the substitution, return `Nothing`

.