|
(* Checking no anomaly on some unexpected intropattern *)
Ltac ih H := induction H as H.
Ltac ih' H H' := induction H as H'.
Goal True -> True.
Fail intro H; ih H.
intro H; ih' H ipattern:([]).
exact I.
Qed.
¤ Dauer der Verarbeitung: 0.0 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.
|
