Idris接口语法

Question

我正在尝试在Idris中编译interface的简单示例。

interface Foo a where
     foo : a -> String

但是我一直收到这个类型检查错误：

error: expected: "with",
argument expression,
function right hand side,
implicit function argument,
with pattern
interface Foo a where 
                ^     

我认为它在逻辑上应该与本教程中的Show接口相同：http://docs.idris-lang.org/en/latest/tutorial/interfaces.html的语法发生了变化吗？或者问题在哪里？

我正在使用Idris版本0.9.12。

Answer 1

在Idris 0.9.12中，现在称为接口的语法是class

class Foo a where
     foo : a -> String