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

Safe Haskell | None

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 LevelAtom |
AbstractTerm PlusLevel |
AbstractTerm Level |
AbstractTerm Sort |
AbstractTerm Type |
AbstractTerm Term |
AbstractTerm a => AbstractTerm [a] |
AbstractTerm a => AbstractTerm (Maybe a) |
AbstractTerm a => AbstractTerm (Ptr a) |
AbstractTerm a => AbstractTerm (Arg a) |
AbstractTerm a => AbstractTerm (Dom a) |
(Subst a, AbstractTerm a) => AbstractTerm (Abs a) |
(AbstractTerm a, AbstractTerm b) => AbstractTerm (a, b) |