<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<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">"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">michel.levy.imag@free.fr</a> <br>
mobile : 06 59 13 42 53<br>
web : michel.levy.imag.free.fr
</div>
</body>
</html>