Module F (X:E). Inductive foo := box : X.T -> foo. End F.
Module ME. Definition T := nat. End ME. Module A := F ME. (* Note: A.foo could live in Set, and coqchk sees that (because of
template polymorphism implementation details) *)
¤ 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 ist noch experimentell.