[Agda] Unicode in Standard Library

[Andrés Sicard-Ramírez]

On 12/02/2008, Shin-Cheng Mu <scm at iis.sinica.edu.tw> wrote:
>
>
> It is probably a good idea to have a "standard prelude"
> for .emacs with a selection of default key bindings
> which mainly covers the symbols used in the standard
> library.


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

("\\llbracket" "⟦")

instead of

-- From the Agda README
("\\[[" "⟦")



All the best,

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20080212/b326db86/attachment.html