在 Idris 2 中选择命名实现

Question

根据这个旧答案，Idris 1 具有

using

语法来选择代码块的默认实现。对应的 Idris 2 语法是什么？

我尝试使用答案中的语法：

using implementation Any
  tick1 : Time -> Writer Bool Time
  tick1 t = pure t

但是这个甚至无法解析：

 `-- src/HL2/Clock.idr line 14 col 0:
     Expected end of input.
     
     HL2.Clock:14:1--14:6
      14 | using implementation Any
           ^^^^^

Answer 1

@{name}

语法允许将自定义实现传递给函数。

[reverseOrd] Ord Nat where
   compare Z (S n)     = GT
   compare (S n) Z     = LT
   compare Z Z         = EQ
   compare (S x) (S y) = compare @{reverseOrd} x y


main : IO ()
main = printLn $ sort @{reverseOrd} [1,2,3,4,5]

此打印

[5, 4, 3, 2, 1]