| 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 760 B |
|
Quelle bug_7392.v Sprache: Coq |
|||||||||
|
Class ElimInv {X Y : Type} (Pout : X -> Y) (Pclose : X -> option Y) :=
elim_inv : False. Class IntoAcc {X Y : Type} (E1 E2 : nat) (α β : X -> Y) := into_acc : False. Global Instance elim_inv_acc_with_close {X Y : Type} E1 E2 α β (foo : nat -> nat -> Y -> Y) : IntoAcc E1 E2 α β -> ElimInv (X:=X) (Y:=Y) α (fun x => Some (foo E1 E2 (β x))). Proof. intros []. Qed. Lemma tac_inv_elim {X Y : Type} Pout Pclose : ElimInv (X:=X) (Y:=Y) Pout Pclose -> False. Proof. intros []. Qed. Global Instance into_acc_na E n : IntoAcc (X:=unit) (Y:=nat) E E (fun _ => 0) (fun _ => 5 + n). Proof. Admitted. Goal False. eapply tac_inv_elim with (Pclose:=(fun xx => Some _)). eapply @elim_inv_acc_with_close. eapply @into_acc_na. (* EXPLOSION *) Abort. ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28