Axiom P : nat -> Prop.
Axiom PS : forall n, P n -> P (S n).
Axiom P0 : P 0.
Hint Resolve PS : foobar.
Hint Resolve P0 : foobar.
Goal P 100.
Proof.
Fail typeclasses eauto 100 with foobar.
typeclasses eauto 101 with foobar.
Abort.
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|