Agda.TypeChecking.Substitute

Application

class Apply t

Abstraction

class Abstract t

Explicit substitutions

class DeBruijn a

Substitution and raisingshiftingweakening

class Subst t a

Telescopes

data TelV a

type ListTel' a

bindsWithHidingToTel'

bindsWithHidingToTel

class TeleNoAbs a

Functions on abstractions

class GetBody a

Syntactic equality and order

Level stuff

data Substitution' a

type Substitution