|
(* Testing the reordering of hypothesis required by pattern, fold and change. *)
Goal forall (A:Set) (x:A) (A':=A), True.
intros.
fold A' in x. (* succeeds: x is moved after A' *)
Undo.
pattern A' in x.
Undo.
change A' in x.
Abort.
(* p and m should be moved before H *)
Goal forall n:nat, n=n -> forall m:nat, let p := (m,n) in True.
intros.
change n with (snd p) in H.
Abort.
¤ Dauer der Verarbeitung: 0.14 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.
|
