Module A. (* Test hiding of a scoped notation by a lonely notation *) Infix"*" := mult'. Checkforall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. End A.
Module B. (* Test that an overridden scoped notation is deactivated *) Infix"*" := mult' : nat_scope. Checkforall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. End B.
¤ 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.0.1Bemerkung:
(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 ist noch experimentell.
