Quelle notation_principal_scope.v Sprache: Coq

Arguments conj {_ _} _ _%_function.

Set Warnings "+inconsistent-scopes".
Fail Notation pp X := (conj X X).

Fail Notation pp := 1 (only printing).

Fail Notation pp X := nonexisting.

Fail Notation pp X := (conj X X) (X, X in scope nat_scope).

Notation pp X := (conj X X) (X in scope nat_scope).

Notation "$" := I (only parsing) : nat_scope.
Notation "$" := (I I) (only parsing) : bool_scope.

Open Scope bool_scope.
Check pp $.
Fail Check pp (id $).

Notation pp1 X := (X%nat) (X in scope bool_scope).
Notation pp2 X := ((X + X)%type) (X in scope bool_scope).
Notation pp3 X := (((X, X)%type, X)%nat) (X in scope bool_scope).

quality100%

¤ Dauer der Verarbeitung: 0.6 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.