| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 262 B |
|
Quelle bug_12566_1.v Sprache: Coq |
|||||||||||||||
|
Class C (n:nat) := c{}. #[export] Instance c0 : C 0 := {}. Definition x := 0. Opaque x. Type _ : C x. (* this is maybe wrong behaviour, if it changes just update the test *) #[export] Hint Opaque x : typeclass_instances. Transparent x. Fail Type _ : C x.
¤ Dauer der Verarbeitung: 0.3 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-04-02