Agda.TypeChecking.MetaVars
findIdx
isBlockedTerm
isEtaExpandable
assignTerm
assignTerm'
newSortMeta
newSortMetaCtx
newTypeMeta
newTypeMeta_
newIFSMeta
newIFSMetaCtx
newNamedValueMeta
newValueMeta
newValueMetaCtx
newValueMeta'
newValueMetaCtx'
newTelMeta
type Condition
trueCondition
newArgsMeta
newArgsMeta'
newArgsMetaCtx
newArgsMetaCtx'
newRecordMeta
newRecordMetaCtx
newQuestionMark
blockTerm
blockTermOnProblem
blockTypeOnProblem
unblockedTester
postponeTypeCheckingProblem_
postponeTypeCheckingProblem
problemType
etaExpandListeners
wakeupListener
etaExpandMetaSafe
data MetaKind
allMetaKinds
etaExpandMeta
etaExpandBlocked
x vs = v
assignV
assignWrapper
assign
assignMeta
assignMeta'
subtypingForSizeLt
expandProjectedVars
etaExpandProjectedVar
class NoProjectedVar a
data ProjVarExc
type FVs
type SubstCand
checkLinearity
type Res
data InvertExcept
inverseSubst
updateMeta
allMetas