Agda.TypeChecking.Rules.Term
isType
isType_
ptsRule
noFunctionsIntoSize
isTypeEqualTo
leqType_
checkTelescope
checkPiTelescope
data LamOrPi
checkTelescope'
checkTypedBindings
checkTypedBinding
checkLambda
checkPostponedLambda
insertHiddenLambdas
checkAbsurdLambda
checkExtendedLambda
checkRecordExpression
checkRecordUpdate
checkLiteral
checkArguments'
checkExpr
checkApplication
domainFree
checkMeta
inferMeta
checkOrInferMeta
inferHeadDef
inferHead
inferDef
checkConstructorApplication
checkHeadApplication
traceCallE
checkArguments
checkArguments_
inferExpr
inferExpr'
defOrVar
checkDontExpandLast
isModuleFreeVar
inferExprForWith
checkLetBindings
checkLetBinding
class ConvColor a i