Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

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
  - isPrefixOf :: a -> a -> Maybe Elims
- abstractTerm :: Type -> Term -> Type -> Term -> TCM Term
- class AbsTerm a where
  - absTerm :: Term -> a -> a
- swap01 :: Subst Term a => a -> a

# Documentation

typeOf :: Type -> Type Source #

abstractType :: Type -> Term -> Type -> TCM Type Source #

`abstractType a v b[v] = b` where `a : v`.

piAbstractTerm :: Term -> Type -> Type -> TCM Type Source #

    piAbstractTerm v a b[v] = (w : a) -> b[w]

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

IsPrefixOf Elims Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Elims -> Elims -> Maybe Elims Source #
IsPrefixOf Term Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Term -> Term -> Maybe Elims Source #
IsPrefixOf Args Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Args -> Args -> Maybe Elims Source #

abstractTerm :: Type -> Term -> Type -> Term -> TCM Term Source #

class AbsTerm a where Source #

Methods

absTerm :: Term -> a -> a Source #

    subst u . absTerm u == id

Instances

AbsTerm LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> LevelAtom -> LevelAtom Source #
AbsTerm PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> PlusLevel -> PlusLevel Source #
AbsTerm Level Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Level -> Level Source #
AbsTerm Sort Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Sort -> Sort Source #
AbsTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Type -> Type Source #
AbsTerm Term Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Term -> Term Source #
AbsTerm a => AbsTerm [a] Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> [a] -> [a] Source #
AbsTerm a => AbsTerm (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Maybe a -> Maybe a Source #
AbsTerm a => AbsTerm (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Dom a -> Dom a Source #
AbsTerm a => AbsTerm (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Arg a -> Arg a Source #
(Subst Term a, AbsTerm a) => AbsTerm (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Abs a -> Abs a Source #
AbsTerm a => AbsTerm (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Elim' a -> Elim' a Source #
(AbsTerm a, AbsTerm b) => AbsTerm (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> (a, b) -> (a, b) Source #

swap01 :: Subst Term a => a -> a Source #

This swaps `var 0` and `var 1`.