Module Rewriting.Substitution

showSubst :: (a -> String) -> Map Int (Term a) -> String   

Transforms a substitution into a string representation.

emptySubst :: Map Int (Term a)   

The empty substitution.

Further infos:

• solution complete, i.e., able to compute all solutions

extendSubst :: Map Int (Term a) -> Int -> Term a -> Map Int (Term a)   

Extends a substitution with a new mapping from the given variable to the given term. An already existing mapping with the same variable will be thrown away.

listToSubst :: [(Int,Term a)] -> Map Int (Term a)   

Returns a substitution that contains all the mappings from the given list. For multiple mappings with the same variable, the last corresponding mapping of the given list is taken.

lookupSubst :: Map Int (Term a) -> Int -> Maybe (Term a)   

Returns the term mapped to the given variable in a substitution or Nothing if no such mapping exists.

applySubst :: Map Int (Term a) -> Term a -> Term a   

Applies a substitution to the given term.

applySubstEq :: Map Int (Term a) -> (Term a,Term a) -> (Term a,Term a)   

Applies a substitution to both sides of the given term equation.

applySubstEqs :: Map Int (Term a) -> [(Term a,Term a)] -> [(Term a,Term a)]   

Applies a substitution to every term equation in the given list.

restrictSubst :: Map Int (Term a) -> [Int] -> Map Int (Term a)   

Returns a new substitution with only those mappings from the given substitution whose variable is in the given list of variables.

composeSubst :: Map Int (Term a) -> Map Int (Term a) -> Map Int (Term a)   

Composes the first substitution phi with the second substitution sigma. The resulting substitution sub fulfills the property sub(t) = phi(sigma(t)) for a term t. Mappings in the first substitution shadow those in the second.