Module M1. Fixpoint stupid (x : nat) : nat := 1.
Reserved Notation" x '==' 1 " (in custom example at level 0, x constr). Notation" x '==' 1" := (stupid x) (in custom example). End M1.
Module M2. Fixpoint stupid (x : nat) : nat := 1. Notation" x '==' 1" := (stupid x) (in custom example at level 0).
Fail Notation" x '==' 1" := (stupid x) (in custom example at level 1). End M2.
Module M3.
Reserved Notation" x '==' 1 " (in custom example at level 55, x constr).
Fixpoint stupid (x : nat) : nat := 1 where" x '==' 1" := (stupid x) (in custom example).
End M3.
Messung V0.5
¤ Dauer der Verarbeitung: 0.14 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 und die Messung sind noch experimentell.
