Agda.TypeChecking.Abstract

Functions for abstracting terms over other terms.

Documentation

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

class IsPrefixOf a where

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

Methods

isPrefixOf :: a -> a -> Maybe Elims

Instances

IsPrefixOf Elims

IsPrefixOf Term

IsPrefixOf Args

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)

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

AbstractTerm a => AbstractTerm (Elim' a)

AbstractTerm a => AbstractTerm (Dom a)

AbstractTerm a => AbstractTerm (Arg a)

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