| 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 1 kB |
|
Quelle bug_4121.v Sprache: Coq |
|||||||||
|
(* -*- coq-prog-args: ("-nois") -*- *)
Unset Strict Universe Declaration. (* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then fro (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897a Declare ML Module "rocq-runtime.plugins.ltac". Set Default Proof Mode "Classic". Set Universe Polymorphism. Class Contr_internal (A : Type) := BuildContr { center : A }. Arguments center A {_}. Class Contr (A : Type) : Type := Contr_is_trunc : Contr_internal A. #[export] Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instance Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A |}. #[export] Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}. Check @contr_paths_contr0@{i}. Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *) (** It should have length 1, just like contr_paths_contr0 *) ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28