[Agda] rewrite keyword

[Philip Wadler]

Unicode and rewriting are both explained in PLFA:
  https://plfa.github.io/Naturals/#unicode
  https://plfa.github.io/Equality/#rewriting
I repeat the explanation of Unicode below. Cheers, -- P

Unicode <https://plfa.github.io/Naturals/#unicode>

This chapter uses the following unicode:

ℕ  U+2115  DOUBLE-STRUCK CAPITAL N (\bN)
→  U+2192  RIGHTWARDS ARROW (\to, \r, \->)
∸  U+2238  DOT MINUS (\.-)
≡  U+2261  IDENTICAL TO (\==)
⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)
⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
∎  U+220E  END OF PROOF (\qed)

Each line consists of the Unicode character (ℕ), the corresponding code
point (U+2115), the name of the character (DOUBLE-STRUCK CAPITAL N), and
the sequence to type into Emacs to generate the character (\bN).

The command \r gives access to a wide variety of rightward arrows. After
typing \r, one can access the many available arrows by using the left,
right, up, and down keys to navigate. The command remembers where you
navigated to the last time, and starts with the same character next time.
The command \l works similarly for left arrows. In place of left, right,
up, and down keys, one may also use control characters:

C-b  left (backward one character)
C-f  right (forward one character)
C-p  up (to the previous line)
C-n  down (to the next line)

We write C-b to stand for control-b, and similarly. One can also navigate
left and right by typing the digits that appear in the displayed list.

For a full list of supported characters, use agda-input-show-translations
 with:

M-x agda-input-show-translations

All the characters supported by agda-mode are shown. We write M-x to stand
for typing ESC followed by x.

If you want to know how you input a specific Unicode character in an agda
file, move the cursor onto the character and use quail-show-key with:

M-x quail-show-key

You’ll see a key sequence of the character in mini buffer. If you run M-x
quail-show-key on say ∸, you will see \.- for the character.


.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/



On Mon, 30 Mar 2020 at 17:00, Georgi Lyubenov <godzbanebane at gmail.com>
wrote:

> Hi!
>
> \^l brings up the superscript 'l' as one of four choices for me - I can
> choose which one I want by using the corresponding number
> [image: 2020-03-30-225522_377x30_scrot.png]
>
> Rewrite is described as being syntactic sugar for 'with' and 'with'
> itself is not a term. What kind of term are you expecting out of the
> 'rewrite'?
>
> =======
> Georgi
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200331/aacaf605/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 2020-03-30-225522_377x30_scrot.png
Type: image/png
Size: 4470 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200331/aacaf605/attachment.png>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200331/aacaf605/attachment.ksh>