| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 490 B |
|
Quelle bug_2017.v Sprache: Coq |
|||||||||||||||
|
(* Some check of Miller's pattern inference - used to fail in 8.2 due first to the presence of aliases, secondly due to the absence of restriction of the potential interesting variables to the subset of variables effectively occurring in the term to instantiate *) Set Implicit Arguments. Parameter choose : forall(P : bool -> Prop)(H : exists x, P x), bool. Parameter H : exists x : bool, True. Definition coef := match Some true with Some _ => @choose _ H |_ => true end .
¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-09-30) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-10-09