Idrisインターフェイスの構文

Question

私はIdrisでinterfaceの簡単な例をコンパイルしようとしています。

interface Foo a where 
    foo : a -> String 

しかし、私は、この型チェックエラー得続ける：私はそれはチュートリアルのShowインターフェイスと論理的に同じであるべきと考えてい

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

：http://docs.idris-lang.org/en/latest/tutorial/interfaces.htmlは、構文が変わりましたか？それともどこに問題がありますか？

私はIdrisバージョン0.9.12を使用しています。イドリス0.9.12で

Answer 1

、今のインターフェイスと呼ばれているもののための構文は次のとおりですclass：

class Foo a where 
    foo : a -> String