| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 570 B |
|
Quelle bug_2320.v Sprache: Coq |
|||||||||||||||
|
(* Managing metavariables in the return clause of a match *) (* This was working in 8.1 but is failing in 8.2 and 8.3. It works in trunk thanks to the new proof engine. It could probably made to work in 8.2 and 8.3 if a return predicate of the form "dummy 0" instead of (or in addition to) a sophisticated predicate of the form "as x in dummy y return match y with 0 => ?P | _ => ID end" *) Inductive dummy : nat -> Prop := constr : dummy 0. Lemma failure : forall (x : dummy 0), x = constr. Proof. intros x. refine (match x with constr => _ end). Abort.
¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet am 2026-09-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-10-09