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 Source

class AbstractTerm a whereSource

Methods

abstractTerm :: Term -> a -> aSource

subst u . abstractTerm u == id