<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">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
</div></div></div>