| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Abstract
Description
Functions for abstracting terms over other terms.
- typeOf :: Type -> Type
- abstractType :: Type -> Term -> Type -> TCM Type
- piAbstractTerm :: Term -> Type -> Type -> TCM Type
- piAbstract :: (Term, EqualityView) -> Type -> TCM Type
- class IsPrefixOf a where
- isPrefixOf :: a -> a -> Maybe Elims
- abstractTerm :: Type -> Term -> Type -> Term -> TCM Term
- class AbsTerm a where
- swap01 :: Subst Term a => a -> a
Documentation
piAbstract :: (Term, EqualityView) -> Type -> TCM Type Source
piAbstract (v, a) b[v] = (w : a) -> b[w]
For rewrite, it does something special:
piAbstract (prf, Eq a v v') b[v,prf] = (w : a) (w' : Eq a w v') -> b[w,w']
class IsPrefixOf a where Source
isPrefixOf u v = Just es if v == u .applyE es
Methods
isPrefixOf :: a -> a -> Maybe Elims Source
Instances
Instances
| AbsTerm LevelAtom Source | |
| AbsTerm PlusLevel Source | |
| AbsTerm Level Source | |
| AbsTerm Sort Source | |
| AbsTerm Type Source | |
| AbsTerm Term Source | |
| AbsTerm a => AbsTerm [a] Source | |
| AbsTerm a => AbsTerm (Maybe a) Source | |
| AbsTerm a => AbsTerm (Ptr a) Source | |
| AbsTerm a => AbsTerm (Dom a) Source | |
| AbsTerm a => AbsTerm (Arg a) Source | |
| (Subst Term a, AbsTerm a) => AbsTerm (Abs a) Source | |
| AbsTerm a => AbsTerm (Elim' a) Source | |
| (AbsTerm a, AbsTerm b) => AbsTerm (a, b) Source |