|
(* A wish granted by the new support for patterns in notations *)
Local Notation mkmatch0 e p
:= match e with
| p => true
| _ => false
end.
Local Notation "'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.12 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.
|
