|
Require List.
Import List.ListNotations.
Variable Foo : nat -> nat.
Delimit Scope Foo_scope with F.
Notation " [ x ] " := (Foo x) : Foo_scope.
Check ([1] : nat)%F.
¤ Dauer der Verarbeitung: 0.15 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.
|
