Agda.TypeChecking.Records
orderFields
insertMissingFields
recordModule
getRecordDef
getRecordOfField
getRecordFieldNames
recordFieldNames
findPossibleRecords
getRecordFieldTypes
getRecordTypeFields
getOriginalProjection
getRecordConstructorType
getRecordConstructor
isRecord
isRecordType
tryRecordType
getDefType
projectTyped
isEtaRecord
isEtaCon
isInductiveRecord
isEtaRecordType
isRecordConstructor
isGeneratedRecordConstructor
unguardedRecord
recursiveRecord
isRecursiveRecord
recRecursive_
etaExpandBoundVar
expandRecordVar
expandRecordVarsRecursively
curryAt
etaExpandRecord
etaExpandRecord_
etaExpandAtRecordType
etaContractRecord
isSingletonRecord
isSingletonRecordModuloRelevance
isSingletonRecord'
isSingletonType
isSingletonTypeModuloRelevance
isSingletonType'
emap