Agda.TypeChecking.Abstract

Functions for abstracting terms over other terms.

Documentation

abstractType :: Type -> Term -> Type -> TCM Type

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

piAbstractTerm :: 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]

piAbstract :: 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']

class IsPrefixOf a where

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

Methods

isPrefixOf :: a -> a -> Maybe Elims

Instances

IsPrefixOf Args

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Args -> Args -> Maybe Elims

IsPrefixOf Elims

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Elims -> Elims -> Maybe Elims

IsPrefixOf Term

Defined in Agda.TypeChecking.Abstract

Methods

isPrefixOf :: Term -> Term -> Maybe Elims

abstractTerm :: Type -> Term -> Type -> Term -> TCM Term

class AbsTerm a where

Methods

absTerm :: Term -> a -> a

subst u . absTerm u == id

Instances

AbsTerm Level

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Level -> Level

AbsTerm PlusLevel

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> PlusLevel -> PlusLevel

AbsTerm Sort

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Sort -> Sort

AbsTerm Term

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Term -> Term

AbsTerm Type

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Type -> Type

AbsTerm a => AbsTerm (Arg a)

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Arg a -> Arg a

(TermSubst a, AbsTerm a) => AbsTerm (Abs a)

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Abs a -> Abs a

AbsTerm a => AbsTerm (Dom a)

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Dom a -> Dom a

AbsTerm a => AbsTerm (Elim' a)

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Elim' a -> Elim' a

AbsTerm a => AbsTerm (Maybe a)

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Maybe a -> Maybe a

AbsTerm a => AbsTerm [a]

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> [a] -> [a]

(AbsTerm a, AbsTerm b) => AbsTerm (a, b)

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> (a, b) -> (a, b)

swap01 :: TermSubst a => a -> a

This swaps var 0 and var 1.

Equality of terms for the sake of with-abstraction.

class EqualSy a where

Methods

equalSy :: a -> a -> Bool

Instances

EqualSy ArgInfo

Ignore origin and free variables.

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: ArgInfo -> ArgInfo -> Bool

EqualSy Level

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Level -> Level -> Bool

EqualSy PlusLevel

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: PlusLevel -> PlusLevel -> Bool

EqualSy Sort

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Sort -> Sort -> Bool

EqualSy Term

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Term -> Term -> Bool

EqualSy Type

Ignores sorts.

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Type -> Type -> Bool

EqualSy a => EqualSy (Arg a)

Ignores irrelevant arguments and modality. (And, of course, origin and free variables).

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Arg a -> Arg a -> Bool

(Subst a, EqualSy a) => EqualSy (Abs a)

Ignores absName.

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Abs a -> Abs a -> Bool

EqualSy a => EqualSy (Dom a)

Ignore the tactic.

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Dom a -> Dom a -> Bool

EqualSy a => EqualSy (Elim' a)

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Elim' a -> Elim' a -> Bool

EqualSy a => EqualSy [a]

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: [a] -> [a] -> Bool