[Agda] Infix in Modules with Parameters

[Guillaume Allais]

For the record, this feature request has been around for close to
4 years now: https://github.com/agda/agda/issues/1235

It would indeed be really nice to have such a thing.

Cheers,
--
gallais

On 18/04/18 20:50, 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/20180419/2f45c7e3/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180419/2f45c7e3/attachment.sig>