| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Abstract
Description
Functions for abstracting terms over other terms.
Synopsis
- 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
- abstractTerm :: Type -> Term -> Type -> Term -> TCM Term
- class AbsTerm a where
- swap01 :: Subst Term a => a -> a
Documentation
piAbstract :: (Term, EqualityView) -> Type -> TCM Type #
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 #
isPrefixOf u v = Just es if v == u .applyE es
Minimal complete definition
Methods
isPrefixOf :: a -> a -> Maybe Elims #
Instances
| IsPrefixOf Elims # | |
Defined in Agda.TypeChecking.Abstract | |
| IsPrefixOf Term # | |
Defined in Agda.TypeChecking.Abstract | |
| IsPrefixOf Args # | |
Defined in Agda.TypeChecking.Abstract | |
Minimal complete definition
Instances
| AbsTerm LevelAtom # | |
| AbsTerm PlusLevel # | |
| AbsTerm Level # | |
| AbsTerm Sort # | |
| AbsTerm Type # | |
| AbsTerm Term # | |
| AbsTerm a => AbsTerm [a] # | |
Defined in Agda.TypeChecking.Abstract | |
| AbsTerm a => AbsTerm (Maybe a) # | |
| AbsTerm a => AbsTerm (Dom a) # | |
| AbsTerm a => AbsTerm (Arg a) # | |
| (Subst Term a, AbsTerm a) => AbsTerm (Abs a) # | |
| AbsTerm a => AbsTerm (Elim' a) # | |
| (AbsTerm a, AbsTerm b) => AbsTerm (a, b) # | |
Defined in Agda.TypeChecking.Abstract | |