syntax - Idris 教程 - 中缀形式的命名实现函数

Question

我正在阅读 named implementations 的教程, 这给出了 Semigroup Nat举个例子:

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

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

如果我想使用 Plus 定义，(<+>) @{PlusNatSemi} Z (S Z)作品。但是有没有办法更中缀地写这个？ Z <+> S Z提示缺乏实现，也没有 Z <+> @{PlusNatSemi} S Z也不Z (<+> @{PlusNatSemi}) S Z工作。

Answer 1

在这种情况下，您需要明确定义要使用的命名实现。

但是 Idris 允许命名实现默认在声明 block 中使用 using 表示法。因此，在您的示例中，它将是这样的:

[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