| 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 271 B |
|
Quelle bug_16903.v Sprache: Coq |
|||||||||||||||
|
Definition pull_match_bool_dep {A B} (P : forall b : bool, A b -> B b) (a : A true) (a' : A false) (b : bool) : P b (if b as b return A b then a else a') = if b as b return B b then P _ a else P _ a' := match b with true => eq_refl | false => eq_refl end.
¤ Dauer der Verarbeitung: 0.3 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-04-02