Agda.Interaction.Imports
data MainInterface
mergeInterface
addImportedThings
scopeCheckImport
data MaybeWarnings' a
type MaybeWarnings
applyFlagsToMaybeWarnings
hasWarnings
alreadyVisited
typeCheckMain
getInterface
getInterface_
getInterface'
isCached
getStoredInterface
typeCheck
chaseMsg
highlightFromInterface
readInterface
writeInterface
removePrivates
createInterface
data WhichWarnings
classifyWarning
classifyWarnings
getAllWarnings'
getAllWarnings
constructIScope
buildInterface
getInterfaceFileHashes
moduleHash
isNewerThan