{"type":"rich","url":"https://zyxwv.hatenadiary.org/entry/20080711/1215746927","html":"<iframe src=\"https://hatenablog-parts.com/embed?url=https%3A%2F%2Fzyxwv.hatenadiary.org%2Fentry%2F20080711%2F1215746927\" title=\" Emacs agda-mode \u306e\u4f7f\u3044\u65b9 - zyxwv\u306e\u65e5\u8a18\" class=\"embed-card embed-blogcard\" scrolling=\"no\" frameborder=\"0\" style=\"display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;\"></iframe>","blog_url":"https://zyxwv.hatenadiary.org/","published":"2008-07-11 12:28:47","version":"1.0","title":" Emacs agda-mode \u306e\u4f7f\u3044\u65b9","provider_url":"https://hatena.blog","width":"100%","height":"190","image_url":null,"categories":["Agda"],"author_url":"https://blog.hatena.ne.jp/zyxwv/","provider_name":"Hatena Blog","author_name":"zyxwv","blog_title":"zyxwv\u306e\u65e5\u8a18","description":"Agda2 \u307e\u3058\u308f\u304b\u3093\u306a\u3044\u3002\u5fc3\u6298\u308c\u305d\u3046\u3002\u3068\u308a\u3042\u3048\u305a agda-mode \u3067\u4f7f\u3044\u65b9\u304c\u308f\u304b\u3063\u305f\u3084\u3064\u3092\u9069\u5f53 \u30e1\u30e2\u3002\u305d\u306e\u3046\u3061\u8ffd\u52a0\u3057\u307e\u3059\u3002 C-c C-x C-l agda \u3067\u8a3c\u660e\u3092\u958b\u59cb\u3002 ? \u8a3c\u660e\u304c\u3088\u304f\u308f\u304b\u3089\u306a\u3044\u3068\u3053\u308d\u306f ? \u3067\u57cb\u3081\u308b\u3002 assoc x y z = ? \u3053\u308c\u3067 C-c C-x C-l \u3068\u3059\u308b\u3068 ? \u304c\u30b4\u30fc\u30eb(\u7528\u6cd5\u304c\u6b63\u3057\u3044\u304b\u4e0d\u660e)\u306b\u306a\u308b\u3002 C-c C-c \u5834\u5408\u5206\u3051\u3092\u81ea\u52d5\u3067\u3084\u3063\u3066\u304f\u308c\u308b\u3002 assoc x y z = {! !} \u304c assoc zero y z = {! !} assoc (suc y) y' z = {! !} \u306b\u306a\u308b\u3002"}