Safe Haskell | None |
---|---|
Language | Haskell2010 |
Implements naive substitution functions for replacing type and term variables.
Synopsis
- substVar :: (name -> Maybe (Term tyname name uni fun a)) -> Term tyname name uni fun a -> Maybe (Term tyname name uni fun a)
- substTyVar :: (tyname -> Maybe (Type tyname uni ann)) -> Type tyname uni ann -> Type tyname uni ann
- typeSubstTyNames :: (tyname -> Maybe (Type tyname uni ann)) -> Type tyname uni ann -> Type tyname uni ann
- termSubstNames :: (name -> Maybe (Term tyname name uni fun a)) -> Term tyname name uni fun a -> Term tyname name uni fun a
- termSubstTyNames :: (tyname -> Maybe (Type tyname uni a)) -> Term tyname name uni fun a -> Term tyname name uni fun a
- bindingSubstNames :: (name -> Maybe (Term tyname name uni fun a)) -> Binding tyname name uni fun a -> Binding tyname name uni fun a
- bindingSubstTyNames :: (tyname -> Maybe (Type tyname uni a)) -> Binding tyname name uni fun a -> Binding tyname name uni fun a
Documentation
substVar :: (name -> Maybe (Term tyname name uni fun a)) -> Term tyname name uni fun a -> Maybe (Term tyname name uni fun a) Source #
Replace a variable using the given function.
substTyVar :: (tyname -> Maybe (Type tyname uni ann)) -> Type tyname uni ann -> Type tyname uni ann Source #
Replace a type variable using the given function.
typeSubstTyNames :: (tyname -> Maybe (Type tyname uni ann)) -> Type tyname uni ann -> Type tyname uni ann Source #
Naively substitute type names (i.e. do not substitute binders).
termSubstNames :: (name -> Maybe (Term tyname name uni fun a)) -> Term tyname name uni fun a -> Term tyname name uni fun a Source #
Naively substitute names using the given functions (i.e. do not substitute binders).
termSubstTyNames :: (tyname -> Maybe (Type tyname uni a)) -> Term tyname name uni fun a -> Term tyname name uni fun a Source #
Naively substitute type names using the given functions (i.e. do not substitute binders).