Agda-2.7.0: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Monad.Base.Types

Contents

Description

Data structures for the type checker.

Part of Agda.TypeChecking.Monad.Base, extracted to avoid import cycles.

Synopsis

Context

type Context = [ContextEntry] Source #

The Context is a stack of ContextEntrys.