Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Abstract
Description
Functions for abstracting terms over other terms.
Documentation
piAbstractTerm :: Term -> Type -> Type -> TypeSource
class AbstractTerm a whereSource
Methods
abstractTerm :: Term -> a -> aSource
subst u . abstractTerm u == id
Produced by Haddock version 2.6.1