| 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 436 B |
|
Quelle bug_3495.v Sprache: Coq |
|||||||||
|
Require Import RelationClasses.
Axiom R : Prop -> Prop -> Prop. #[export] Declare Instance R_refl : Reflexive R. Class bar := { x : False }. Record foo := { a : Prop ; b : bar }. Definition default_foo (a0 : Prop) `{b : bar} : foo := {| a := a0 ; b := b |}. Goal exists k, R k True. Proof. eexists. evar (b : bar). let e := match goal with |- R ?e _ => constr:(e) end in unify e (a (default_foo True)). subst b. reflexivity. Abort. ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28