плохо. не надо их делать:)

ну то есть идея базируется на интерактивной разработке. Изменил что-то - пробуешь. Либо C-c C-l для всего буфера, но чаще работаешь с дыркой (hole, goal). Про неё обычно знаешь тип и окружение (C-c C-,), задача сводится к тому чтобы из окружения собрать что-то нужного типа, часто с новой дыркой. Тут подробнее
http://wiki.portal.chalmers.se/agda/agda.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode