<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<tt>For the record, this feature request has been around for close
to<br>
4 years now: <a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/1235">https://github.com/agda/agda/issues/1235</a><br>
<br>
It would indeed be really nice to have such a thing.<br>
<br>
Cheers,<br>
--<br>
gallais<br>
</tt><br>
<div class="moz-cite-prefix">On 18/04/18 20:50, 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>