| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Abstract

Description
Functions for abstracting terms over other terms.
Documentation

piAbstractTerm :: Term -> Type -> Type -> Type | Source

class AbstractTerm a where | Source

Methods

abstractTerm :: Term -> a -> a | Source

    subst u . abstractTerm u == id

Instances

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)

Produced by Haddock version 2.4.2