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