[Agda] Infix in Modules with Parameters

[Dr. ERDI Gergo]

On Thu, 19 Apr 2018, Philip Wadler wrote:

> Thanks. Wow, that looks incredibly ugly. When invoking the module, what would one pass
> to instantiate the second parameter? Cheers, -- P

Those lets are not parameters of the module, so if you have e.g.

module X (A : Set) (_≤_ : A → A → Bool)(let _≤_ = _≤_; infix 1 _≤_)(_⊝_ : A → A → A)(let _⊝_ = _⊝_; infix 1 _⊝_)(zero : A) where

you can still instantiate it with four arguments.