(* 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.
Messung V0.5
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
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 und die Messung sind noch experimentell.
