| 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 188 B |
|
Quellcode-Bibliothek bug_5097.v Sprache: Coq |
|||||||||
|
(* Tracing existing evars along the weakening rule ("clear") *)
Goal forall y, exists x, x=0->x=y. intros. eexists ?[x]. intros. let x:=constr:(ltac:(clear y; exact 0)) in idtac x. 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.14Bemerkung: (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
