| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Data.Rewriting.Substitution
Synopsis
- data GSubst v f v'
- type Subst f v = GSubst v f v
- gApply :: Ord v => GSubst v f v' -> Term f v -> Maybe (Term f v')
- apply :: Ord v => Subst f v -> Term f v -> Term f v
- compose :: Ord v => Subst f v -> Subst f v -> Subst f v
- data GSubst v f v'
- type Subst f v = GSubst v f v
- module Data.Rewriting.Substitution.Ops
- module Data.Rewriting.Substitution.Match
- module Data.Rewriting.Substitution.Unify
- module Data.Rewriting.Substitution.Pretty
- module Data.Rewriting.Substitution.Parse
Documentation
A generalised? substitution: a finite, partial map from variables to terms with a different variable type.
type Subst f v = GSubst v f v Source #
A substitution, mapping variables to terms. Substitutions are equal to the identity almost everywhere.
Important operations
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.
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.
compose :: Ord v => Subst f v -> Subst f v -> Subst f v Source #
Compose substitutions. We have
(s1 `compose` s2) `apply` t = s1 `apply` (s2 `apply` t).
Reexported modules
A generalised? substitution: a finite, partial map from variables to terms with a different variable type.