Open
Description
With Agda 2.6.1 we'll have new commands such as -vprofile.definitions:10 and -vprofile.modules:10 which allows one to time the type checking of different modules and definitions.
In #1101 @UlfNorell manages to shave 5 seconds off by simply changing one proof, so it seems like there are potentially big gains to be had.