Data.Rewriting.Substitution.Type

Documentation

type Subst f v = GSubst v f v

A substitution, mapping variables to terms. Substitutions are equal to the identity almost everywhere.

data GSubst v f v'

A generalised? substitution: a finite, partial map from variables to terms with a different variable type.

Instances

(Show v, Show v', Show f) => Show (GSubst v f v')

Defined in Data.Rewriting.Substitution.Type

Methods

showsPrec :: Int -> GSubst v f v' -> ShowS

show :: GSubst v f v' -> String

showList :: [GSubst v f v'] -> ShowS

(Pretty v, Pretty f, Pretty v') => Pretty (GSubst v f v')

Defined in Data.Rewriting.Substitution.Pretty

Methods

pretty :: GSubst v f v' -> Doc

prettyList :: [GSubst v f v'] -> Doc

utilities not reexported from Substitution

fromMap :: Map v (Term f v') -> GSubst v f v'

toMap :: GSubst v f v' -> Map v (Term f v')