Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Cobol/Test-Suite/SQL M/ (Apache Web Server Version 2.4.65^©) Datei vom 4.1.2008 mit Größe 29 kB

Quelle bug_12908.v Sprache: unbekannt

Definition mult' m n := 2 * m * n.

Module A.
(* Test hiding of a scoped notation by a lonely notation *)
Infix "*" := mult'.
Check forall 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.
Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
End B.