| 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 1006 B |
|
Quelle bug_9971.v Sprache: Coq |
|||||||||
|
(* Test that it raises a normal error and not an anomaly *)
Set Primitive Projections. Record prod A B := pair { fst : A ; snd : B }. Arguments fst {A B} _. Arguments snd {A B} _. Arguments pair {A B} _ _. Record piis := { dep_types : Type; indep_args : dep_types -> Type }. Import EqNotations. Goal forall (id : Set) (V : id) (piiio : id -> piis) (Z : {ridc : id & prod (dep_types (piiio ridc)) True}) (P : dep_types (piiio V) -> Type) (W : {x : dep_types (piiio V) & P x}), let ida := fun (x : id) (y : dep_types (piiio x)) => indep_args (piiio x) y in prod True (ida V (projT1 W)) -> Z = existT _ V (pair (projT1 W) I) -> ida (projT1 Z) (fst (projT2 Z)). intros. refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))] H in let v := I in _); refine (snd X). Undo. Fail refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))] H in let v := I in snd X). Abort. ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28