Safe Haskell | None |
---|---|
Language | Haskell98 |
Functions for abstracting terms over other terms.
- piAbstractTerm :: Term -> Type -> Type -> Type
- class IsPrefixOf a where
- isPrefixOf :: a -> a -> Maybe Elims
- class AbstractTerm a where
- abstractTerm :: Term -> a -> a
Documentation
class IsPrefixOf a where Source
isPrefixOf u v = Just es
if v == u
.applyE
es
isPrefixOf :: a -> a -> Maybe Elims Source
class AbstractTerm a where Source
abstractTerm :: Term -> a -> a Source
subst u . abstractTerm u == id
AbstractTerm LevelAtom Source | |
AbstractTerm PlusLevel Source | |
AbstractTerm Level Source | |
AbstractTerm Sort Source | |
AbstractTerm Type Source | |
AbstractTerm Term Source | |
AbstractTerm a => AbstractTerm [a] Source | |
AbstractTerm a => AbstractTerm (Maybe a) Source | |
AbstractTerm a => AbstractTerm (Ptr a) Source | |
(Subst a, AbstractTerm a) => AbstractTerm (Abs a) Source | |
AbstractTerm a => AbstractTerm (Elim' a) Source | |
AbstractTerm a => AbstractTerm (Dom a) Source | |
AbstractTerm a => AbstractTerm (Arg a) Source | |
(AbstractTerm a, AbstractTerm b) => AbstractTerm (a, b) Source |