<div dir="ltr">Unicode and rewriting are both explained in PLFA:<div>  <a href="https://plfa.github.io/Naturals/#unicode">https://plfa.github.io/Naturals/#unicode</a></div><div>  <a href="https://plfa.github.io/Equality/#rewriting">https://plfa.github.io/Equality/#rewriting</a><div><div>I repeat the explanation of Unicode below. Cheers, -- P</div><div><br></div><div><h2 id="gmail-unicode" style="margin:0px 0px 15px;padding:0px;font-weight:400;font-size:32px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";background-color:rgb(253,253,253)">Unicode<a class="gmail-anchorjs-link" href="https://plfa.github.io/Naturals/#unicode" style="color:rgb(23,86,169);text-decoration-line:none;opacity:0;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal;font-size:1em;line-height:1;font-family:anchorjs-icons;padding-left:0.375em"></a></h2><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">This chapter uses the following unicode:</p><div class="gmail-language-plaintext gmail-highlighter-rouge" style="color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)"><div class="gmail-highlight" style="margin-bottom:15px;background:rgb(238,238,255)"><pre class="gmail-highlight" style="margin-top:0px;margin-bottom:15px;padding:0.4em;font-size:15px;border:1px dashed rgb(201,225,246);border-radius:3px;background-image:initial;background-position:initial;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;overflow-x:auto;break-inside:avoid"><code style="font-size:0.85em;border:0px;border-radius:3px;padding:1px 0px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif">ℕ  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)
</code></pre></div></div><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">Each line consists of the Unicode character (<code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">ℕ</code>), the corresponding code point (<code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">U+2115</code>), the name of the character (<code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">DOUBLE-STRUCK CAPITAL N</code>), and the sequence to type into Emacs to generate the character (<code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">\bN</code>).</p><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">The command <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">\r</code> gives access to a wide variety of rightward arrows. After typing <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">\r</code>, 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 <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">\l</code> works similarly for left arrows. In place of left, right, up, and down keys, one may also use control characters:</p><div class="gmail-language-plaintext gmail-highlighter-rouge" style="color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)"><div class="gmail-highlight" style="margin-bottom:15px;background:rgb(238,238,255)"><pre class="gmail-highlight" style="margin-top:0px;margin-bottom:15px;padding:0.4em;font-size:15px;border:1px dashed rgb(201,225,246);border-radius:3px;background-image:initial;background-position:initial;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;overflow-x:auto;break-inside:avoid"><code style="font-size:0.85em;border:0px;border-radius:3px;padding:1px 0px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif">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)
</code></pre></div></div><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">We write <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">C-b</code> to stand for control-b, and similarly. One can also navigate left and right by typing the digits that appear in the displayed list.</p><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">For a full list of supported characters, use <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">agda-input-show-translations</code> with:</p><div class="gmail-language-plaintext gmail-highlighter-rouge" style="color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)"><div class="gmail-highlight" style="margin-bottom:15px;background:rgb(238,238,255)"><pre class="gmail-highlight" style="margin-top:0px;margin-bottom:15px;padding:0.4em;font-size:15px;border:1px dashed rgb(201,225,246);border-radius:3px;background-image:initial;background-position:initial;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;overflow-x:auto;break-inside:avoid"><code style="font-size:0.85em;border:0px;border-radius:3px;padding:1px 0px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif">M-x agda-input-show-translations
</code></pre></div></div><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">All the characters supported by <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">agda-mode</code> are shown. We write M-x to stand for typing <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">ESC</code> followed by <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">x</code>.</p><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">If you want to know how you input a specific Unicode character in an agda file, move the cursor onto the character and use <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">quail-show-key</code> with:</p><div class="gmail-language-plaintext gmail-highlighter-rouge" style="color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)"><div class="gmail-highlight" style="margin-bottom:15px;background:rgb(238,238,255)"><pre class="gmail-highlight" style="margin-top:0px;margin-bottom:15px;padding:0.4em;font-size:15px;border:1px dashed rgb(201,225,246);border-radius:3px;background-image:initial;background-position:initial;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;overflow-x:auto;break-inside:avoid"><code style="font-size:0.85em;border:0px;border-radius:3px;padding:1px 0px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif">M-x quail-show-key
</code></pre></div></div><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">You’ll see a key sequence of the character in mini buffer. If you run <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">M-x quail-show-key</code> on say <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">∸</code>, you will see <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">\.-</code> for the character.</p><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)"><br></p><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div><br></div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 30 Mar 2020 at 17:00, Georgi Lyubenov <<a href="mailto:godzbanebane@gmail.com">godzbanebane@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Hi!<br><br>\^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<div><img src="cid:ii_k8ew6z8d0" alt="2020-03-30-225522_377x30_scrot.png" width="377" height="30"><br><br>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'?<br><br>=======<br>Georgi</div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>