| 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 623 B |
|
Quelle bug_5401.v Sprache: Coq |
|||||||||
|
(* Testing printing of bound unnamed variables in pattern printer *)
Module A. Parameter P : nat -> Type. Parameter v : forall m, P m. Parameter f : forall (P : nat -> Type), (forall a, P a) -> P 0. Class U (R : P 0) (m : forall x, P x) : Prop. #[export] Instance w : U (f _ (fun _ => v _)) v := {}. Print HintDb typeclass_instances. End A. (* #5731 *) Module B. Axiom rel : Type -> Prop. Axiom arrow_rel : forall {A1}, A1 -> rel A1. Axiom forall_rel : forall E, (forall v1 : Type, E v1 -> rel v1) -> Prop. Axiom inl_rel: forall_rel _ (fun _ => arrow_rel). #[export] Hint Resolve inl_rel : foo. Print HintDb foo. End B. ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28