<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi Michel,<br>
<br>
Re 1) in general many inputs are behind menus. If you input \^l
you should get a menu at the bottom that you can choose other
options from.<br>
If you copy paste a symbol into emacs, select it and call
describe-char, it should also tell you how to input it using
agda-input.<br>
<br>
Others can probably answer your question about rewrite better than
I can :)<br>
<br>
Cheers,<br>
<br>
<br>
Arjen<br>
</p>
<div class="moz-cite-prefix">On 3/30/20 9:49 PM, Michel Levy wrote:<br>
</div>
<blockquote type="cite"
cite="mid:67e36203-d243-0448-0928-6ac4331298e3@free.fr">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<p>In an exercise of <a class="moz-txt-link-freetext"
href="https://plfa.github.io/Relations/"
moz-do-not-send="true">https://plfa.github.io/Relations/</a>
You have the following definition</p>
<p><a id="17419" href="https://plfa.github.io/Relations/#17419"
class="Function" moz-do-not-send="true">+-monoˡ-≤</a> <a
id="17429" class="Symbol" moz-do-not-send="true">:</a> <a
id="17431" class="Symbol" moz-do-not-send="true">∀</a> <a
id="17433" class="Symbol" moz-do-not-send="true">(</a><a
id="17434"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17434"
class="Bound" moz-do-not-send="true">m</a> <a id="17436"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17436"
class="Bound" moz-do-not-send="true">n</a> <a id="17438"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17438"
class="Bound" moz-do-not-send="true">p</a> <a id="17440"
class="Symbol" moz-do-not-send="true">:</a> <a id="17442"
href="https://plfa.github.io/Relations/Agda.Builtin.Nat.html#165"
class="Datatype" moz-do-not-send="true">ℕ</a><a id="17443"
class="Symbol" moz-do-not-send="true">)</a> <a id="17447"
class="Symbol" moz-do-not-send="true">→</a> <a id="17449"
href="https://plfa.github.io/Relations/#17434" class="Bound"
moz-do-not-send="true">m</a> <a id="17451"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#1195"
class="Datatype Operator" moz-do-not-send="true">≤</a> <a
id="17453"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17436"
class="Bound" moz-do-not-send="true">n</a> <a id="17475"
class="Symbol" moz-do-not-send="true">→</a> <a id="17477"
href="https://plfa.github.io/Relations/#17434" class="Bound"
moz-do-not-send="true">m</a> <a id="17479"
href="https://plfa.github.io/Relations/Agda.Builtin.Nat.html#298"
class="Primitive Operator" moz-do-not-send="true">+</a> <a
id="17481"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17438"
class="Bound" moz-do-not-send="true">p</a> <a id="17483"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#1195"
class="Datatype Operator" moz-do-not-send="true">≤</a> <a
id="17485"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17436"
class="Bound" moz-do-not-send="true">n</a> <a id="17487"
href="https://plfa.github.io/Relations/Agda.Builtin.Nat.html#298"
class="Primitive Operator" moz-do-not-send="true">+</a> <a
id="17489"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17438"
class="Bound" moz-do-not-send="true">p</a> </p>
<p><a id="17491" href="https://plfa.github.io/Relations/#17419"
class="Function" moz-do-not-send="true">+-monoˡ-≤</a> <a
id="17501"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17501"
class="Bound" moz-do-not-send="true">m</a> <a id="17503"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17503"
class="Bound" moz-do-not-send="true">n</a> <a id="17505"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17505"
class="Bound" moz-do-not-send="true">p</a> <a id="17507"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17507"
class="Bound" moz-do-not-send="true">m≤n</a> <a id="17512"
class="Keyword" moz-do-not-send="true">rewrite</a> <a
id="17520"
href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911"
class="Function" moz-do-not-send="true">+-comm</a> <a
id="17527"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17501"
class="Bound" moz-do-not-send="true">m</a> <a id="17529"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17505"
class="Bound" moz-do-not-send="true">p</a> <a id="17531"
class="Symbol" moz-do-not-send="true">|</a> <a id="17533"
href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911"
class="Function" moz-do-not-send="true">+-comm</a> <a
id="17540"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17503"
class="Bound" moz-do-not-send="true">n</a> <a id="17542"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17505"
class="Bound" moz-do-not-send="true">p</a> <a id="17545"
class="Symbol" moz-do-not-send="true">=</a> <a id="17547"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#16619"
class="Function" moz-do-not-send="true">+-monoʳ-≤</a> <a
id="17557"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17505"
class="Bound" moz-do-not-send="true">p</a> <a id="17559"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17501"
class="Bound" moz-do-not-send="true">m</a> <a id="17561"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17503"
class="Bound" moz-do-not-send="true">n</a> <a id="17563"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17507"
class="Bound" moz-do-not-send="true">m≤n</a></p>
<p>On this example, I have two questions</p>
<p><br>
1) How to have the superscript l in the name +-monol</p>
<p>On my emacs \^l give a right to left superscript arrow</p>
<p><br>
</p>
<p>2) Why </p>
<p><a id="17491" href="https://plfa.github.io/Relations/#17419"
class="Function" moz-do-not-send="true">+-monoˡ-≤</a> <a
id="17501"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17501"
class="Bound" moz-do-not-send="true">m</a> <a id="17503"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17503"
class="Bound" moz-do-not-send="true">n</a> <a id="17505"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17505"
class="Bound" moz-do-not-send="true">p</a> <a id="17507"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17507"
class="Bound" moz-do-not-send="true">m≤n</a> <a id="17512"
class="Keyword" moz-do-not-send="true">rewrite</a> <a
id="17520"
href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911"
class="Function" moz-do-not-send="true">+-comm</a> <a
id="17527"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17501"
class="Bound" moz-do-not-send="true">m</a> <a id="17529"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17505"
class="Bound" moz-do-not-send="true">p</a> <a id="17531"
class="Symbol" moz-do-not-send="true">|</a> <a id="17533"
href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911"
class="Function" moz-do-not-send="true">+-comm</a> <a
id="17540"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17503"
class="Bound" moz-do-not-send="true">n</a> <a id="17542"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17505"
class="Bound" moz-do-not-send="true">p</a> <br>
</p>
<p>is not a term ? </p>
<p>To understand the meaning of rewrite, I try to get the type of</p>
<p><a id="17491" href="https://plfa.github.io/Relations/#17419"
class="Function" moz-do-not-send="true">\lambda m n p m</a><a
id="17507"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17507"
class="Bound" moz-do-not-send="true">≤</a><a id="17491"
href="https://plfa.github.io/Relations/#17419"
class="Function" moz-do-not-send="true">n -> ag+-monoˡ-≤</a>
<a id="17501"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17501"
class="Bound" moz-do-not-send="true">m</a> <a id="17503"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17503"
class="Bound" moz-do-not-send="true">n</a> <a id="17505"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17505"
class="Bound" moz-do-not-send="true">p</a> <a id="17507"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17507"
class="Bound" moz-do-not-send="true">m≤n</a> <a id="17512"
class="Keyword" moz-do-not-send="true">rewrite</a> <a
id="17520"
href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911"
class="Function" moz-do-not-send="true">+-comm</a> <a
id="17527"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17501"
class="Bound" moz-do-not-send="true">m</a> <a id="17529"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17505"
class="Bound" moz-do-not-send="true">p</a> <a id="17531"
class="Symbol" moz-do-not-send="true">|</a> <a id="17533"
href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911"
class="Function" moz-do-not-send="true">+-comm</a> <a
id="17540"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17503"
class="Bound" moz-do-not-send="true">n</a> <a id="17542"
href="https://plfa.github.io/Relations/plfa.part1.Relations.html#17505"
class="Bound" moz-do-not-send="true">p</a><br>
</p>
<p>But this is not a term, and I got a parse error.</p>
<p>More generally, why isn't there a term of the form (exp1
rewrite exp2) ?</p>
<p>PS : I have read the doc
<a class="moz-txt-link-rfc2396E"
href="https://agda.readthedocs.io/en/latest/language/with-abstraction.html#with-rewrite"
moz-do-not-send="true">"https://agda.readthedocs.io/en/latest/language/with-abstraction.html#with-rewrite"</a><br>
</p>
<div class="moz-signature">-- <br>
courriel : <a class="moz-txt-link-abbreviated"
href="mailto:michel.levy.imag@free.fr" moz-do-not-send="true">michel.levy.imag@free.fr</a>
<br>
mobile : 06 59 13 42 53<br>
web : michel.levy.imag.free.fr </div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</body>
</html>