Fehlermeldung: "Klasse" ist veraltet, Quelle enthält keine Klasse

Question

Ich habe gerade Idris v.1.0 installiert und führe den Beispielcode aus dem Proof section von Rosetta Code Stück für Stück aus. Alles funktioniert gut bis zum folgenden Fragment, das die erzeugt Das Schlüsselwort 'class' ist veraltet. Verwenden Sie stattdessen "Schnittstelle". Fehler.

-- 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 

Es gibt kein einziges Stück "Klasse" in der Quelle. Was könnte hinter diesem Problem stehen?

Answer 1

Das sind nur Warnungen. Die -Anmerkungen sind in thisveraltet Kapitel des Handbuchs beschrieben. Sie können sie sicher löschen und den Beweis beenden, z. wie folgt:

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