|
Require Import JMeq.
Axiom test : forall n m : nat, JMeq n m.
Goal forall n m : nat, JMeq n m.
(* I) with no intros nor variable hints, this should produce a regular error
instead of Uncaught exception Failure("nth"). *)
Fail rewrite test.
(* II) with intros but indication of variables, still an error *)
Fail (intros; rewrite test).
(* III) a working variant: *)
intros; rewrite (test n m).
Abort.
¤ Dauer der Verarbeitung: 0.13 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.
|
