Search code examples
idris

Error message says 'class' is deprecated, source does not contain 'class'

I've just installed Idris v.1.0 and run the sample code from the Proof section of Rosetta Code, piece by piece. Everything works fine up to the following fragment, which produces the The 'class' keyword is deprecated. Use 'interface' instead. error.

-- 3.1, Prove that the addition of any two even numbers is even. 

evensPlus1 : {a : MyNat} -> {b : MyNat} -> (EvNat a) -> (EvNat b) -> (EvNat (a :+ b))
evensPlus1 ea eb = ?proof31

There's not a single piece of 'class' in the source. What could be behind this issue?

Solution

  • Those are just warnings. The %elim-annotations are described in this deprecated chapter of the manual. You can safely delete them and finish the proof, e.g. like this:

    evensPlus1 : (EvNat a) -> (EvNat b) -> (EvNat (a :+ b))
evensPlus1 EvO eb = eb
evensPlus1 (EvSS y) eb = EvSS (evensPlus1 y eb)

congS : {a : MyNat} ->  {b : MyNat} -> (a = b) -> (S a = S b)
congS Refl = Refl