| 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 598 B |
|
Quelle bug_2006.v Sprache: Coq |
|||||||||
|
(* Take the type constraint on Record into account *)
Definition Type1 := Type. Fail Record R : Type1 := { p:Type1 }. (* was accepted before trunk revision 11619 *) (* Remarks: - The behaviour was inconsistent with the one of Inductive, e.g. Inductive R : Type1 := Build_R : Type1 -> R. was correctly refused. - CoRN makes some use of the following configuration: Definition CProp := Type. Record R : CProp := { ... }. CoRN may have to change the CProp definition into a notation if the preservation of the former semantics of Record type constraints turns to be required. *) ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28