| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Abstract
Description
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
Methods
isPrefixOf :: a -> a -> Maybe Elims Source
Instances
class AbstractTerm a where Source
Instances
| AbstractTerm LevelAtom | |
| AbstractTerm PlusLevel | |
| AbstractTerm Level | |
| AbstractTerm Sort | |
| AbstractTerm Type | |
| AbstractTerm Term | |
| AbstractTerm a => AbstractTerm [a] | |
| AbstractTerm a => AbstractTerm (Maybe a) | |
| AbstractTerm a => AbstractTerm (Ptr a) | |
| (Subst a, AbstractTerm a) => AbstractTerm (Abs a) | |
| AbstractTerm a => AbstractTerm (Elim' a) | |
| AbstractTerm a => AbstractTerm (Dom a) | |
| AbstractTerm a => AbstractTerm (Arg a) | |
| (AbstractTerm a, AbstractTerm b) => AbstractTerm (a, b) |