<br><div><span class="gmail_quote">On 12/02/2008, <b class="gmail_sendername">Shin-Cheng Mu</b> <<a href="mailto:scm@iis.sinica.edu.tw">scm@iis.sinica.edu.tw</a>> wrote:</span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>It is probably a good idea to have a "standard prelude"<br>for .emacs with a selection of default key bindings<br>which mainly covers the symbols used in the standard<br>library. </blockquote></div><br>It is a good idea. Moreover, the key bindings should be the "standard" TeX ones. For example, the left semantics bracket should be defined by<br>
<br>("\\llbracket" "⟦") <br><br>instead of<br><br>-- From the Agda README<br>("\\[[" "⟦") <br><br><br><br>All the best,<br><br>-- <br>Andrés