Agda.TypeChecking.Abstract

Functions for abstracting terms over other terms.

Documentation

piAbstractTerm :: Term -> Type -> Type -> Type

class AbstractTerm a where

Methods

abstractTerm :: Term -> a -> a

subst u . abstractTerm u == id

Instances

AbstractTerm LevelAtom

AbstractTerm PlusLevel

AbstractTerm Level

AbstractTerm Sort

AbstractTerm Type

AbstractTerm Term

AbstractTerm a => AbstractTerm [a]

AbstractTerm a => AbstractTerm (Maybe a)

AbstractTerm a => AbstractTerm (Ptr a)

AbstractTerm a => AbstractTerm (Arg a)

AbstractTerm a => AbstractTerm (Dom a)

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

(AbstractTerm a, AbstractTerm b) => AbstractTerm (a, b)