Quelle bug_11046.v Sprache: Coq

From Ltac2 Require Import Ltac2.

Ltac2 Type t := [..].
Ltac2 Type t ::= [A(int)].

(* t cannot be extended with two constructors with the same name *)
Fail Ltac2 Type t ::= [A(bool)].
Fail Ltac2 Type t ::= [B | B(bool)].

(* constructors cannot be shadowed in the same module *)
Fail Ltac2 Type s := [A].

(* constructors with the same name can be defined in distinct modules *)
Module Other.
Ltac2 Type t ::= [A(bool)].
End Other.
Module YetAnother.
Ltac2 Type t := [A].
End YetAnother.

quality99%

¤ Dauer der Verarbeitung: 0.13 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.