DeclareScope blafu. DelimitScope blafu with B. Axiom DoesNotMatch : Type. Axiom consumer : forall {A} (B : A -> Type) (E:Type) (x : A) (ls : list nat), unit.
Notation"| p1 | .. | pn" := (@cons _ p1 .. (@cons _ pn nil) ..) (at level 91) : blafu. Notation"'mmatch_do_not_write' x 'in' T 'as' y 'return' 'M' p 'with_do_not_write' ls" :=
(@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B)
(at level 200, ls at level 91, only parsing). Notation"'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
(mmatch_do_not_write x in T as y return M p with_do_not_write ls)
(at level 200, ls at level 91, p at level 10, only parsing). (* This should not gives a warning *) Notation"'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
(@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B)
(at level 200, ls at level 91, p at level 10, only printing,
format "'[ ' mmatch '/' x ']' '/' '[ ' in '/' T ']' '/' '[ ' as '/' y ']' '/' '[ ' return M p ']' with '//' '[' ls ']' '//' end"
). (* Check use of "mmatch" *) Check (mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x return M (x = x) with | 1 end).
(* 2nd example *) Notation"#" := I (at level 0, only parsing). Notation"#" := I (at level 0, only printing). Check #. Notation"##" := I (at level 0, only printing). Notation"##" := I (at level 0, only parsing). Check ##.
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.
