|
(* Using tactic "change" under binders *)
Definition add2 n := n +2.
Goal (fun n => n) = (fun n => n+2).
change (?n + 2) with (add2 n).
match goal with |- _ = (fun n => add2 n) => idtac end. (* To test the presence of add2 *)
Abort.
¤ Dauer der Verarbeitung: 0.18 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.
|
