Fail Ltac2 my_change1 (a : constr) (b : constr) := change $a with $b.
Fail Ltac2 my_change2 (a:preterm) (b:constr) := change $preterm:a with $b.
(* This is pretty bad, maybe $x should mean $pattern:x in patterns? Main question is if we allow preterm in pattern, is "fun x => let y := preterm:($x) in pattern:($preterm:y)" going to be confusing? (x must be constr, and we error at runtime??)
Instead don't allow preterms, instead expose "pattern_of_preterm : preterm -> pattern", having runtime errors there seems more sensible than with the quotation.
*)
Ltac2 my_change3 (a:pattern) (b:constr) := change $pattern:a with $b.
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.
