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

Question

我正在阅读有关命名实现的教程，其中给出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工作。

标签： syntaxidris

Answer 1

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

但是Idris默认情况下允许命名实现在带有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