| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 581 B |
|
Quelle bug_9329.v Sprache: Coq |
|||||||||
|
(* Declare empty levels in the same order they are computed *)
Notation "< a ; b ; c >1" := (sum a (sum b c)) (at level 18, a at level 19, b at level 20, c at level 21). Notation "< a ; b ; c >2" := (sum a (sum b c)) (at level 28, a at level 29, c at level 32, b at level 31). Notation "< a ; b ; c >3" := (sum a (sum b c)) (at level 38, c at level 42, a at level 39, b at level 41). Notation "< a ; b ; c >4" := (sum a (sum b c)) (at level 48, c at level 52, b at level 51, a at level 49). Notation "< a ; b >" := (sum a b) (at level 61, a at level 63, b at level 62). ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28