<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>