ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Abstract

Functions for abstracting terms over other terms.

valueabstractType :: Type -> Term -> Type -> TCM Type

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

valuepiAbstractTerm :: ArgInfo -> Term -> Type -> Type -> TCM Type

piAbstractTerm NotHidden v a b[v] = (w : a) -> b[w] piAbstractTerm Hidden v a b[v] = {w : a} -> b[w]

valuepiAbstract :: Arg (Term, EqualityView) -> Type -> TCM Type

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

For the inspect idiom, it does something special: @piAbstract (v, a) b[v] = (w : a) {w' : Eq a w v} -> 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']

classclass IsPrefixOf a where

isPrefixOf u v = Just es if v == u applyE es.

Instances3IsPrefixOf

valueabstractTerm :: Type -> Term -> Type -> Term -> TCM Term

classclass AbsTerm a where

Instances12AbsTerm, …

AbsTerm LevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
AbsTerm PlusLevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
AbsTerm SortDefined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
AbsTerm TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
AbsTerm TypeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
AbsTerm a => AbsTerm (Arg a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
AbsTerm a => AbsTerm (Dom a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
AbsTerm a => AbsTerm (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
AbsTerm a => AbsTerm (Maybe a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
AbsTerm a => AbsTerm [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
(TermSubst a, AbsTerm a) => AbsTerm (Abs a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
(AbsTerm a, AbsTerm b) => AbsTerm (a, b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract

valueswap01 :: TermSubst a => a -> a

This swaps var 0 and var 1.

Equality of terms for the sake of with-abstraction.

1 declaration

classclass EqualSy a where

Instances11EqualSy, …

EqualSy ArgInfoDefined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
Ignore origin and free variables.
EqualSy LevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
EqualSy PlusLevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
EqualSy SortDefined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
EqualSy TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
EqualSy TypeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
Ignores sorts.
EqualSy a => EqualSy (Arg a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
Ignores irrelevant arguments and modality. (And, of course, origin and free variables).
EqualSy a => EqualSy (Dom a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
Ignore the tactic.
EqualSy a => EqualSy (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
EqualSy a => EqualSy [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
(Subst a, EqualSy a) => EqualSy (Abs a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
Ignores absName.