Safe Haskell | Safe |
---|---|
Language | Haskell98 |
Capture avoiding substitution of witnesses in expressions.
If a binder would capture a variable then it is anonymized to deBruijn form.
- class SubstituteWX c where
- substituteWX :: (Ord n, SubstituteWX c) => Bind n -> Witness a n -> c a n -> c a n
- substituteWXs :: (Ord n, SubstituteWX c) => [(Bind n, Witness a n)] -> c a n -> c a n
Documentation
class SubstituteWX c where Source #
substituteWX :: (Ord n, SubstituteWX c) => Bind n -> Witness a n -> c a n -> c a n Source #
Wrapper for substituteWithWX
that determines the set of free names in the
type being substituted, and starts with an empty binder stack.
substituteWXs :: (Ord n, SubstituteWX c) => [(Bind n, Witness a n)] -> c a n -> c a n Source #
Wrapper for substituteWithWX
to substitute multiple things.