Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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 :: ArgInfo -> Term -> Type -> Type -> TCM Type Source #

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 Source #

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 Source #

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

Methods

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

Instances

Instances details
IsPrefixOf Args Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

IsPrefixOf Elims Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

IsPrefixOf Term Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

class AbsTerm a where Source #

Methods

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

subst u . absTerm u == id

Instances

Instances details
AbsTerm Level Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Level -> Level Source #

AbsTerm PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

AbsTerm Sort Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Sort -> Sort Source #

AbsTerm Term Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

AbsTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Type -> Type Source #

AbsTerm a => AbsTerm (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

(TermSubst 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 (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Dom a -> Dom 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 (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

AbsTerm a => AbsTerm [a] Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> [a] -> [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 :: TermSubst a => a -> a Source #

This swaps var 0 and var 1.

Equality of terms for the sake of with-abstraction.

class EqualSy a where Source #

Methods

equalSy :: a -> a -> Bool Source #

Instances

Instances details
EqualSy ArgInfo Source #

Ignore origin and free variables.

Instance details

Defined in Agda.TypeChecking.Abstract

EqualSy Level Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Level -> Level -> Bool Source #

EqualSy PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

EqualSy Sort Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Sort -> Sort -> Bool Source #

EqualSy Term Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Term -> Term -> Bool Source #

EqualSy Type Source #

Ignores sorts.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Type -> Type -> Bool Source #

EqualSy a => EqualSy (Arg a) Source #

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

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Arg a -> Arg a -> Bool Source #

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

Ignores absName.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Abs a -> Abs a -> Bool Source #

EqualSy a => EqualSy (Dom a) Source #

Ignore the tactic.

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Dom a -> Dom a -> Bool Source #

EqualSy a => EqualSy (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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

EqualSy a => EqualSy [a] Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

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