ну то есть идея базируется на интерактивной разработке. Изменил что-то - пробуешь. Либо C-c C-l для всего буфера, но чаще работаешь с дыркой (hole, goal). Про неё обычно знаешь тип и окружение (C-c C-,), задача сводится к тому чтобы из окружения собрать что-то нужного типа, часто с новой дыркой. Тут подробнее http://wiki.portal.chalmers.se/agda/agda.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2012-11-26 03:53 pm (UTC)ну то есть идея базируется на интерактивной разработке. Изменил что-то - пробуешь. Либо C-c C-l для всего буфера, но чаще работаешь с дыркой (hole, goal). Про неё обычно знаешь тип и окружение (C-c C-,), задача сводится к тому чтобы из окружения собрать что-то нужного типа, часто с новой дыркой. Тут подробнее
http://wiki.portal.chalmers.se/agda/agda.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode