Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- 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
Minimal complete definition
Instances
AbsTerm LevelAtom # | |
AbsTerm PlusLevel # | |
AbsTerm Level # | |
AbsTerm Sort # | |
AbsTerm Type # | |
AbsTerm Term # | |
AbsTerm a => AbsTerm [a] # | |
AbsTerm a => AbsTerm (Maybe a) # | |
AbsTerm a => AbsTerm (Ptr 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) # | |