Closed
Description
At the moment if you want to type check everything in an Agda library you either have to manually list every "important" file you want to type check or you have to write code to automatically generate an Everything.agda file, usually using a modified version of the Haskell script in the standard library.
My suggestion is to make it so that you could run agda on an agda-lib file as well as agda files. Running agda myLib.agda-lib would type check every .agda file found under the directories specified by the include part of the agda-lib file.