Idris 2中选择命名实现的对应语法是什么？

Idris 1 中的 using implementation 语法可用于为代码块指定默认实现，Idris 2 已移除该语法，改用 default 关键字实现相同功能。

你尝试的 Idris 1 风格代码：

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
           ^^^^^

Idris 2 的正确写法：

default Any
  tick1 : Time -> Writer Bool Time
  tick1 t = pure t

default 关键字后紧跟目标实现名称，缩进范围内的代码块会默认使用该实现，功能与 Idris 1 的 using implementation 完全一致。

内容的提问来源于stack exchange，提问作者Cactus