| 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 539 B |
|
Quelle bug_17314.v Sprache: Coq |
|||||||||||||||
|
Definition arrow_apply (f : Prop -> Prop) := True -> f True. (* We need True-> to trigger a unificatio Definition something (x : Prop) := arrow_apply (fun _ => x). Axiom trivial: forall l1: Prop, something l1 -> something l1. Lemma t : exists f, arrow_apply f. eexists. unshelve apply trivial. (* was giving "something ?l1@{t:=_UNBOUND_REL_1}" while the evar is not supposed to depend on (* so, we check that, indeed, t is not here *) match goal with [ H : True |- _ ] => fail 1 | _ => idtac end. Abort.
¤ Dauer der Verarbeitung: 0.2 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-04-02