| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 317 B |
|
Quelle bug_15864.vSprache: Coq |
|||||||||||||||
|
Require Import Ltac2.Ltac2. (* This line is copied from https://coq.inria.fr/refman/proof-engine/ltac2.html *) Notation "[ x ]" := ltac2:(let x := Ltac2.Constr.pretype x in exact $x) (only parsing). Check [ 1 ]. Notation "<< y >>" := [ y + y ] (only parsing). Check << 3 * 3 >>. Check eq_refl : 18 = << 3 * 3 >>.
¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-06-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-27