Automation for documenting Agda code

In recent work I spent more time trying to properly typeset Agda tokens that appear in documentation than on making sure the prose is correct and well-written.

To address this, I suggest we develop a script that reads in the tex produced by agda (from our .lagda files) and extracts all tokens along with the appropriate tex macros for formatting them and places these in a macro file. With such a utility, we can simply use, e.g., \GovAction instead of \AgdaRecord{GovAction} in the documentation.

It might seem this merely saves a few key strokes but the problem when documenting a large Agda module (especially when you're not the original author of the module) is that it can be tedious and distracting to try to remember or look up whether we want, e.g., \AgdaRecord{GovAction} instead of \AgdaDatatype{GovAction}.