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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Abstract

Description

Functions for abstracting terms over other terms.

Synopsis

Documentation

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.

Minimal complete definition

isPrefixOf

Methods

isPrefixOf :: a -> a -> Maybe Elims Source #

Instances
IsPrefixOf Elims Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

IsPrefixOf Term Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

IsPrefixOf Args Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

class AbsTerm a where Source #

Minimal complete definition

absTerm

Methods

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

subst u . absTerm u == id
Instances
AbsTerm LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

AbsTerm PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

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.