Agda.TypeChecking.Rules.Term

Types

isType

isType_

ptsRule

noFunctionsIntoSize

isTypeEqualTo

leqType_

Telescopes

checkTelescope

checkPiTelescope

data LamOrPi

checkTelescope'

checkTypedBindings

checkTypedBinding

Lambda abstractions

checkLambda

checkPostponedLambda

insertHiddenLambdas

checkAbsurdLambda

checkExtendedLambda

catchIlltypedPatternBlockedOnMeta

Records

expandModuleAssigns

checkRecordExpression

checkRecordUpdate

Literal

checkLiteral

Terms

checkArguments'

checkExpr

quoteGoal

quoteContext

checkApplication

unquoteM

unquoteTactic

domainFree

Meta variables

checkMeta

inferMeta

checkOrInferMeta

Applications

inferHeadDef

inferHead

inferDef

checkConstructorApplication

checkHeadApplication

traceCallE

checkArguments

checkArguments_

inferExpr

inferExpr'

defOrVar

checkDontExpandLast

isModuleFreeVar

inferExprForWith

Let bindings

checkLetBindings

checkLetBinding