(* Example from #9521 *) Declare Custom Entry expr.
Module A.
Notation"expr0:( s )" := s (s custom expr at level 0). Notation"#" := 0 (in custom expr at level 1). Check expr0:(#). (* Should not be an anomaly "unknown level 0" *)
End A.
(* Another example from a comment at #11561 *)
Module B.
Declare Custom Entry special. Notation"## x" := (S x) (in custom expr at level 10, x custom special at level 10). Notation"[ e ]" := e (e custom expr at level 10). Notation"1" := 1 (in custom special). Check [ ## 1 ].
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.
