| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/LibreOffice/icon-themes/sifr/cmd/ (LibreOffice Version 25.8.3.2©) Datei vom 5.10.2025 mit Größe 484 B |
|
Quellcode-Bibliothek bug_4480.v Sprache: Coq |
|||||||||||||||
|
Require Import Setoid. Definition proj (P Q : Prop) := P. Lemma foo (P : Prop) : proj P P = P. Admitted. Lemma trueI : True <-> True. Admitted. Goal True. Fail setoid_rewrite foo. Fail setoid_rewrite trueI. 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-10