(* A wish granted by the new support for patterns in notations *)
LocalNotation mkmatch0 e p
:= match e with
| p => true
| _ => false end. LocalNotation"'mkmatch' [[ e ]] [[ p ]]"
:= match e with
| p => true
| _ => false end
(at level 0, p pattern). Check mkmatch0 _ ((0, 0)%core). Check mkmatch [[ _ ]] [[ ((0, 0)%core) ]].
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
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.
