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

在伊德里斯0.9.12，對於現在所謂的接口語法是class：

class Foo a where 
    foo : a -> String