Quelle bug_2603.v Sprache: Coq

(** Namespace of module vs. namescope of definitions/constructors/...

As noticed by A. Appel in bug #2603, module names and definition
names used to be in the same namespace. But conflict with names
of constructors (or 2nd mutual inductive...) used to not be checked
enough, leading to strange situations.

- In 8.3pl3 we introduced checks that forbid uniformly the following
  situations.

- For 8.4 we finally managed to make module names and other names
  live in two separate namespace, hence allowing all of the following
  situations.
*)

Module Type T.
End T.

Declare Module K : T.

Module Type L.
Declare Module E : T.
End L.

Module M1 : L with Module E:=K.
Module E := K.
Inductive t := E. (* Used to be accepted, but End M1 below was failing *)
End M1.

Module M2 : L with Module E:=K.
Inductive t := E.
Module E := K. (* Used to be accepted *)
End M2. (* Used to be accepted *)

quality98%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.