| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/output/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 415 B |
|
Quelle bug_10803.v Sprache: Coq |
|||||||||||||||
|
Inductive Foo := foo. Declare Scope foo_scope. Delimit Scope foo_scope with foo. Bind Scope foo_scope with Foo. Notation "'!'" := foo : foo_scope. Definition of_foo {x : nat} {y : nat} (f : Foo) := f. Notation a := (@of_foo O). Notation b := (@a). Check a !. Check @a O !. Check @b O. Check @b O !. (* was failing *) (* All are printed "a !", without making explicit the "0", which is incidentally disputable *)
¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-04-04