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

class AbstractTerm a where

Methods

abstractTerm :: Term -> a -> a

subst u . abstractTerm u == id