|
(* Testing ill-typed rewrite which used to succeed in 8.3 *)
Goal
forall (N : nat -> Prop) (g : nat -> sig N) (IN : forall a : sig N, a = g 0),
N 0 -> False.
Proof.
intros.
Fail rewrite IN in H.
Abort.
¤ Dauer der Verarbeitung: 0.16 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.
|
