<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p>I'm not sure if or where it's documented, but here's a trick I
      use: place a `let` declaration in with the module parameters. See
      `M2` below.</p>
    <p>```agda<br>
      module M1 (_<_ : Set → Set → Set) where<br>
        postulate <br>
          A : Set<br>
          C : (A < A) < A<br>
      <br>
      module M2 (_<_ : Set → Set → Set) (let _<_ = _<_; infixl
      5 _<_) where<br>
        postulate <br>
          A : Set<br>
          C : A < A < A<br>
      ```<br>
    </p>
    <br>
    <div class="moz-cite-prefix">On 04/18/2018 11:50 AM, Philip Wadler
      wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAESRbco2SkRzBZY+gJQ+1afh3M3tEr1mjpO-3i9jDa-1vhkW+g@mail.gmail.com">
      <div dir="ltr">Consider the following simple variant of an example
        in the user manual.
        <div><br>
        </div>
        <div>---<br>
          <div><br>
          </div>
          <div>
            <div>open import Data.List using (List; _∷_; [])<br>
            </div>
            <div>open import Data.Bool using (Bool; true; false)</div>
            <div><br>
            </div>
            <div>module Sort(A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A →
              A)(zero : A) where</div>
            <div><br>
            </div>
            <div>  infix 1 _≤_</div>
            <div>  infix 2 _⊝_</div>
            <div><br>
            </div>
            <div>  insert : A → List A → List A</div>
            <div>  insert x [] = x ∷ []</div>
            <div>  insert x (y ∷ ys) with zero ≤ (y ⊝ x)</div>
            <div>  insert x (y ∷ ys)    | true  = x ∷ y ∷ ys</div>
            <div>  insert x (y ∷ ys)    | false = y ∷ insert x ys</div>
            <div><br>
            </div>
            <div>  sort : List A → List A</div>
            <div>  sort []       = []</div>
            <div>  sort (x ∷ xs) = insert x (sort xs)</div>
            <div><br>
            </div>
            <div>---</div>
            <div><br>
            </div>
            <div>This works fine. But now say I add infix declarations
              in so I can omit parentheses.</div>
            <div><br>
            </div>
            <div>---</div>
            <div><br>
            </div>
            <div>
              <div>open import Data.List using (List; _∷_; [])<br>
              </div>
              <div>open import Data.Bool using (Bool; true; false)</div>
              <div><br>
              </div>
              <div>module Sort(A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A
                → A)(zero : A) where</div>
              <div><br>
              </div>
              <div>  infix 1 _≤_</div>
              <div>  infix 2 _⊝_</div>
              <div><br>
              </div>
              <div>  insert : A → List A → List A</div>
              <div>  insert x [] = x ∷ []</div>
              <div>  insert x (y ∷ ys) with zero ≤ (y ⊝ x)</div>
              <div>  insert x (y ∷ ys)    | true  = x ∷ y ∷ ys</div>
              <div>  insert x (y ∷ ys)    | false = y ∷ insert x ys</div>
              <div><br>
              </div>
              <div>  sort : List A → List A</div>
              <div>  sort []       = []</div>
              <div>  sort (x ∷ xs) = insert x (sort xs)</div>
            </div>
            <div><br>
            </div>
            <div>---</div>
            <div><br>
            </div>
            <div>This yields the error message:</div>
            <div><br>
            </div>
            <div>
              <blockquote class="gmail_quote" style="margin:0px 0px 0px
                0.8ex;border-left:1px solid
                rgb(204,204,204);padding-left:1ex">/Users/wadler/sf/src/extra/ModuleInfix.agda:8,11-14<br>
                The following names are not declared in the same scope
                as their<br>
                syntax or fixity declaration (i.e., either not in scope
                at all,<br>
                imported from another module, or declared in a super
                module): _≤_<br>
                _⊝_<br>
                when scope checking the declaration<br>
                  module Sort (A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A
                → A)<br>
                              (zero : A) where</blockquote>
            </div>
            <div><br>
            </div>
            <div>Moving the infix declarations before the module yields
              a similar error message.</div>
            <div><br>
            </div>
            <div>1. What is the right way to declare fixity of infix
              parameters to a module?</div>
            <div>2. Where is this documented?</div>
            <div><br>
            </div>
            <div>Cheers, -- P</div>
            <div><br>
            </div>
            <div><br>
            </div>
            <div><br>
            </div>
            <div><br>
            </div>
            <div>
              <div class="gmail_signature">
                <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" moz-do-not-send="true">http://homepages.inf.ed.ac.uk/wadler/</a></span></div>
                  </div>
                </div>
              </div>
            </div>
          </div>
        </div>
      </div>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <br>
      <pre wrap="">The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
</pre>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <br>
      <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>
    <br>
  </body>
</html>