Idris Tutorial - Functions of named implementations in infix form

Question

I'm reading through the tutorial for named implementations, which gives Semigroup Nat as an example:

[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[MultNatSemi] Semigroup Nat where
  (<+>) x y = x * y

If I wanted to use the Plus definition, (<+>) @{PlusNatSemi} Z (S Z) works. But is there a way to write this more infix-ly? Z <+> S Z complains about a lack of implementation, and neither Z <+> @{PlusNatSemi} S Z nor Z (<+> @{PlusNatSemi}) S Z work.

Answer 1

In this case you need to explicitly define, which named implementations to use.

But Idris allows named implementations to be available by default in a block of declarations with using notation. Thus, in your example, it's going to be like:

[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[MultNatSemi] Semigroup Nat where
  (<+>) x y = x * y

using implementation PlusNatSemi
  semiPlus : Nat -> Nat -> Nat
  semiPlus x y = x <+> y

using implementation MultNatSemi
  semiMul : Nat -> Nat -> Nat
  semiMul x y = x <+> y