Agda.TypeChecking.Rules.Term

Types

isType

isType_

isTypeEqualTo

leqType_

Telescopes

checkTelescope_

checkTypedBindings_

data LamOrPi

checkTypedBindings

checkTypedBinding

Lambda abstractions

checkLambda

checkAbsurdLambda

checkExtendedLambda

Records

checkRecordExpression

checkRecordUpdate

Literal

checkLiteral

Terms

checkArguments'

checkExpr

checkApplication

domainFree

Meta variables

checkMeta

inferMeta

checkOrInferMeta

Applications

inferHeadDef

inferHead

inferDef

checkConstructorApplication

checkHeadApplication

traceCallE

checkArguments

checkArguments_

inferExpr

defOrVar

checkDontExpandLast

isModuleFreeVar

inferExprForWith

Let bindings

checkLetBindings

checkLetBinding

class ConvColor a i