|
(* Checking support for scope delimiters and as clauses in 'pat
applied to notations with binders *)
Notation "'multifun' x .. y 'in' f" := (fun x => .. (fun y => f) .. )
(at level 200, x binder, y binder, f at level 200).
Check multifun '((x, y)%core as z) in (x+y,0)=z.
¤ Dauer der Verarbeitung: 0.14 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.
|
