Agda.TypeChecking.Monad.Base

# Type checking state

data TCState

data FreshThings

initState

stBuiltinThings

## Interface

data ModuleInfo

type VisitedModules

type DecodedModules

data Interface

## Closure

data Closure a

buildClosure

## Constraints

type ConstraintClosure

data Constraint

data Comparison

type Constraints

# Open things

data Open a

# Judgements

data Judgement t a

## Meta variables

data MetaVariable

data MetaInstantiation

data MetaPriority

type MetaInfo

type MetaStore

normalMetaPriority

lowMetaPriority

highMetaPriority

getMetaInfo

getMetaScope

getMetaEnv

getMetaSig

## Interaction meta variables

type InteractionPoints

data InteractionId

## Signature

data Signature

type Sections

type Definitions

data Section

emptySignature

data DisplayForm

data DisplayTerm

defaultDisplayForm

data Definition

type HaskellCode

type HaskellType

type EpicCode

data HaskellRepresentation

data Polarity

data Occurrence

data Defn

defIsRecord

data Fields

data Reduced no yes

data IsReduced

data MaybeReduced a

type MaybeReducedArgs

notReduced

reduced

data PrimFun

defClauses

defCompiled

data Delayed

defDelayed

defAbstract

## Injectivity

data FunctionInverse

data TermHead

## Mutual blocks

data MutualId

## Statistics

type Statistics

## Trace

data Call

## Builtin things

type BuiltinThings pf

data Builtin pf

# Type checking environment

data TCEnv

initEnv

## Context

type Context

data ContextEntry

data CtxId

## Let bindings

type LetBindings

## Abstract mode

data AbstractMode

# Type checking errors

data Occ

data OccPos

data TypeError

data TCErr'

data TCErr

# Type checking monad transformer

data TCMT m a

type TCM

class MonadTCM tcm

catchError_

mapTCMT

pureTCM

patternViolation

internalError

typeError

runTCM

runTCM'