Safe Haskell | Safe |
---|---|
Language | Haskell98 |
Capture avoiding substitution of types in expressions.
If a binder would capture a variable then it is anonymized to deBruijn form.
- class SubstituteTX c where
- substituteTX :: (SubstituteTX c, Ord n) => Bind n -> Type n -> c n -> c n
- substituteTXs :: (SubstituteTX c, Ord n) => [(Bind n, Type n)] -> c n -> c n
- substituteBoundTX :: (SubstituteTX c, Ord n) => Bound n -> Type n -> c n -> c n
Documentation
class SubstituteTX c where Source #
SubstituteTX Type Source # | |
SubstituteTX Bind Source # | |
SubstituteTX (Witness a) Source # | |
SubstituteTX (Cast a) Source # | |
SubstituteTX (Alt a) Source # | |
SubstituteTX (Exp a) Source # | |
substituteTX :: (SubstituteTX c, Ord n) => Bind n -> Type n -> c n -> c n Source #
substituteTXs :: (SubstituteTX c, Ord n) => [(Bind n, Type n)] -> c n -> c n Source #
Wrapper for substituteT
to substitute multiple types.
substituteBoundTX :: (SubstituteTX c, Ord n) => Bound n -> Type n -> c n -> c n Source #