Agda.TypeChecking.Monad.Base
data TCState
class ReadTCState m
data PreScopeState
type DisambiguatedNames
data PostScopeState
data PersistentTCState
data LoadedFileCache
type CachedTypeCheckLog
type CurrentTypeCheckLog
data TypeCheckAction
class HasFresh i
data ProblemId
class FreshName a
type ModuleToSource
type SourceToModule
data ModuleInfo
type VisitedModules
type DecodedModules
data Interface
data Closure a
type Constraints
data ProblemConstraint
data Constraint
data Comparison
data CompareDirection
data Open a
data Judgement a
data MetaVariable
data Listener
data Frozen
data MetaInstantiation
data TypeCheckingProblem
data MetaPriority
data RunMetaOccursCheck
data MetaInfo
type MetaNameSuggestion
data NamedMeta
type MetaStore
data InteractionPoint
type InteractionPoints
data Signature
type Sections
type Definitions
type RewriteRuleMap
type DisplayForms
data Section
data DisplayForm
data DisplayTerm
data NLPat
type PElims
type RewriteRules
data RewriteRule
data Definition
type HaskellCode
type HaskellType
type EpicCode
type JSCode
data HaskellExport
data CoreRepresentation
data Polarity
data ExtLamInfo
data Projection
data EtaEquality
data Defn
data Fields
data Simplification
data Reduced no yes
data IsReduced
data MaybeReduced a
type MaybeReducedArgs
type MaybeReducedElims
data AllowedReduction
type AllowedReductions
data PrimFun
type FunctionInverse
data FunctionInverse' c
data TermHead
data MutualId
type Statistics
data Call
type InstanceTable
type TempInstanceTable
data BuiltinDescriptor
data BuiltinInfo
type BuiltinThings pf
data Builtin pf
data HighlightingLevel
data HighlightingMethod
data TCEnv
type Context
data ContextEntry
data CtxId
type LetBindings
data AbstractMode
data ExpandHidden
data ExplicitToInstance
data Candidate
data Occ
data OccPos
data CallInfo
data TerminationError
data SplitError
data UnquoteError
data TypeError
data LHSOrPatSyn
data TCErr
data ReduceEnv
data ReduceM a
data TCMT m a
type TCM
class MonadTCM tcm
type IM