<div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
d) With this,  emacs  still shows correctly specific math symbols<br>
   in the  .adga  files,<br>
but I cannot correctly _input_ these math symbols. For example,<br>
my program<br>
          open import Nat<br>
          ...<br>
          f : \bn<br>
          f = zero<br>
does not compile, the compiler takes  \bn  as lambda.<br>
<br>
Please, how to fix the setting?<br>
<br></blockquote><div><br></div><div>You need to activate the Agda input method. For example:</div><div><br></div><div>M-x set-input-method</div><div><br></div><div>and type Agda at the prompt.</div><div><br></div><div>Another useful shortcut to know is C-\</div>
<div>(Use M-x describe-key C-\ for the doc.)</div><div><br></div><div>Cheers,</div><div>JP.</div></div>