Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Abstract

Description

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 Sort |
AbstractTerm Type |
AbstractTerm Term |
AbstractTerm a => AbstractTerm [a] |
AbstractTerm a => AbstractTerm (Arg a) |
(Subst a, AbstractTerm a) => AbstractTerm (Abs a) |
(AbstractTerm a, AbstractTerm b) => AbstractTerm (a, b) |