| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/output/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 300 B |
|
Quelle bug_20188.vSprache: Coq |
|||||||||||||||
|
Require Import Ltac2.Ltac2. Notation "[[ x ]]" := ltac2:(()) (only parsing). Notation "[ x ]" := ltac2:(let x := Ltac2.Constr.pretype x in exact $x) (only parsing). Fail Check foo. (* Error: The reference foo was not found in the current environment. *) Check [[ foo ]]. (* success *) Check [ foo ].
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09