[Agda] Infix in Modules with Parameters

[Martin Stone Davis]

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.

```agda
module M1 (_<_ : Set → Set → Set) where
   postulate
     A : Set
     C : (A < A) < A

module M2 (_<_ : Set → Set → Set) (let _<_ = _<_; infixl 5 _<_) where
   postulate
     A : Set
     C : A < A < A
```


On 04/18/2018 11:50 AM, Philip Wadler wrote:
> Consider the following simple variant of an example in the user manual.
>
> ---
>
> open import Data.List using (List; _∷_; [])
> open import Data.Bool using (Bool; true; false)
>
> module Sort(A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A → A)(zero : A) where
>
>   infix 1 _≤_
>   infix 2 _⊝_
>
>   insert : A → List A → List A
>   insert x [] = x ∷ []
>   insert x (y ∷ ys) with zero ≤ (y ⊝ x)
>   insert x (y ∷ ys)    | true  = x ∷ y ∷ ys
>   insert x (y ∷ ys)    | false = y ∷ insert x ys
>
>   sort : List A → List A
>   sort []       = []
>   sort (x ∷ xs) = insert x (sort xs)
>
> ---
>
> This works fine. But now say I add infix declarations in so I can omit 
> parentheses.
>
> ---
>
> open import Data.List using (List; _∷_; [])
> open import Data.Bool using (Bool; true; false)
>
> module Sort(A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A → A)(zero : A) where
>
>   infix 1 _≤_
>   infix 2 _⊝_
>
>   insert : A → List A → List A
>   insert x [] = x ∷ []
>   insert x (y ∷ ys) with zero ≤ (y ⊝ x)
>   insert x (y ∷ ys)    | true  = x ∷ y ∷ ys
>   insert x (y ∷ ys)    | false = y ∷ insert x ys
>
>   sort : List A → List A
>   sort []       = []
>   sort (x ∷ xs) = insert x (sort xs)
>
> ---
>
> This yields the error message:
>
>     /Users/wadler/sf/src/extra/ModuleInfix.agda:8,11-14
>     The following names are not declared in the same scope as their
>     syntax or fixity declaration (i.e., either not in scope at all,
>     imported from another module, or declared in a super module): _≤_
>     _⊝_
>     when scope checking the declaration
>       module Sort (A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A → A)
>                   (zero : A) where
>
>
> Moving the infix declarations before the module yields a similar error 
> message.
>
> 1. What is the right way to declare fixity of infix parameters to a 
> module?
> 2. Where is this documented?
>
> Cheers, -- P
>
>
>
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180418/f9f23ab9/attachment.html>