Agda.TypeChecking.Telescope
data OutputTypeName
getOutputTypeName
renameP
renaming
renamingR
flattenTel
reorderTel
reorderTel_
unflattenTel
teleNames
teleArgNames
teleArgs
teleNamedArgs
permuteTel
varDependencies
data SplitTel
splitTelescope
splitTelescopeExact
instantiateTelescope
expandTelescopeVar
telView
telViewUpTo
telViewUpTo'
mustBePi
ifPi
ifPiType
ifNotPi
ifNotPiType
piApplyM
piApply1
intro1
addTypedInstance
resolveUnknownInstanceDefs
getInstanceDefs