Agda.TypeChecking.Substitute

Documentation

class Apply t where

Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).

Methods

apply :: t -> Args -> t

Instances

Apply Permutation

Apply ClauseBody

Apply Clause

Apply Telescope

Apply Sort

Apply Type

Apply Term

Apply FunctionInverse

Apply PrimFun

Apply Defn

Apply Definition

Apply DisplayTerm

Apply t => Apply [t]

Apply t => Apply (Maybe t)

Apply t => Apply (Blocked t)

(Apply a, Apply b) => Apply (a, b)

Apply v => Apply (Map k v)

(Apply a, Apply b, Apply c) => Apply (a, b, c)

piApply :: Type -> Args -> Type

The type must contain the right number of pis without have to perform any reduction.

class Abstract t where

(abstract args v) args --> v[args].

Methods

abstract :: Telescope -> t -> t

Instances

Abstract Permutation

Abstract ClauseBody

Abstract Clause

Abstract Telescope

Abstract Sort

Abstract Type

Abstract Term

Abstract FunctionInverse

Abstract PrimFun

Abstract Defn

Abstract Definition

Abstract t => Abstract [t]

Abstract t => Abstract (Maybe t)

Abstract v => Abstract (Map k v)

abstractArgs :: Abstract a => Args -> a -> a

class Subst t where

Substitute a term for the nth free variable.

Methods

substs :: [Term] -> t -> t

substUnder :: Nat -> Term -> t -> t

Instances

Subst Pattern

Subst ClauseBody

Subst Telescope

Subst Sort

Subst Type

Subst Term

Subst DisplayTerm

Subst Equality

Subst AsBinding

Subst DotPatternInst

Subst a => Subst [a]

Subst a => Subst (Maybe a)

Subst a => Subst (Arg a)

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

Subst t => Subst (Blocked t)

(Subst a, Subst b) => Subst (a, b)

idSub :: Telescope -> [Term]

subst :: Subst t => Term -> t -> t

absApp :: Subst t => Abs t -> Term -> t

Instantiate an abstraction

class Raise t where

Add k to index of each open variable in x.

Methods

raiseFrom :: Nat -> Nat -> t -> t

Instances

Raise Telescope

Raise Sort

Raise Type

Raise Term

Raise DisplayTerm

Raise DisplayForm

Raise AsBinding

Raise t => Raise [t]

Raise t => Raise (Maybe t)

Raise t => Raise (Arg t)

Raise t => Raise (Abs t)

Raise t => Raise (Blocked t)

(Raise a, Raise b) => Raise (a, b)

Raise v => Raise (Map k v)

raise :: Raise t => Nat -> t -> t

data TelView

Constructors

TelV Telescope Type

telView :: Type -> TelView

telePi :: Telescope -> Type -> Type

telePi_ :: Telescope -> Type -> Type

Everything will be a pi.

dLub :: Sort -> Abs Sort -> Sort