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