Agda.TypeChecking.Monad.Base

Type checking state

data TCState

Interface

data ModuleInfo
data Interface

Closure

data Closure a

Constraints

data Constraint
data Comparison

Open things

data Open a

Judgements

data Judgement t a

Meta variables

type MetaInfo
type MetaStore

Interaction meta variables

Signature

data Signature
type Sections
data Section
data Definition
data Polarity
data Occurrence
data Defn
data Fields
data Reduced no yes
data PrimFun
data Delayed

Injectivity

data TermHead

Mutual blocks

data MutualId

Statistics

type Statistics

Trace

type CallTrace
data Call

Builtin things

type BuiltinThings pf
data Builtin pf

Type checking environment

data TCEnv

Context

type Context
data CtxId

Let bindings

Abstract mode

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