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