Idris 2 中的隐式转换？

问题描述

隐式转换在 Idris 2 中仍然可用吗？这个 Idris 1 代码

data Foo : Type -> Type where
  MkFoo : t -> Foo t

public export implicit
IntFoo : Int -> Foo Int
IntFoo = MkFoo

现在无法在 Idris 2 中编译

Error: Parse error at line 95:1:
Couldn't parse declaration (next
tokens: [public,export,implicit,identifier IntFoo,symbol :,identifier Int,symbol ->,identifier Foo,identifier IntFoo])

移动 implicit 并不能修复它，如果我删除 implicit，它编译得很好。

顺便说一句，我查看了从 1 更新到 2 的文档，但看不到任何相关信息。如果你知道在哪里看，一个链接也很好。

解决方法

Idris 2 不支持隐式转换。I believe their exclusion is deliberate。