Idris interface syntax

Question

I am trying to compile simple example of interface in Idris.

interface Foo a where
     foo : a -> String

But I keep getting this type-checking error:

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

I believe it should be logically the same as the Show interface in the tutorial: http://docs.idris-lang.org/en/latest/tutorial/interfaces.html Has the syntax changed? Or where could be the problem?

I am using Idris version 0.9.12.

Answer 1

In Idris 0.9.12, the syntax for what is now called interfaces is class:

class Foo a where
     foo : a -> String