| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 690 B |
|
Quellcode-Bibliothek bug_10762.v Sprache: Coq |
|||||||||||||||
|
Set Implicit Arguments. Generalizable Variables A B. Parameter val: Type. Class Enc (A:Type) : Type := make_Enc { enc : A -> val }. #[export] Hint Mode Enc + : typeclass_instances. Parameter bar : forall A (EA:Enc A), EA = EA. Parameter foo : forall (P:Prop), P -> P = P -> True. Parameter id : forall (P:Prop), P -> P. Check enc. Lemma test : True. eapply foo; [ eapply bar | apply id]. apply id. (* eapply bar introduces an unresolved typeclass evar that is no longer a candidate after the application (eapply should leave typeclass goals shelved). We ensure that this happens also _across_ goals in `[ | ]` and not only at `.`.. *) Abort.
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.12Bemerkung: (vorverarbeitet am 2026-09-29) ¤*Bot Zugriff |
|
||||||||||||||
2026-10-09