Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_3228.v Sprache: Coq

Original von: 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.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.