ModuleType BAR. DeclareModuleImport foo : FOO. Parameter f : forall A, P A -> Q A -> A. End BAR.
ModuleType BAZ. DeclareModuleExport foo : FOO. Parameter g : forall A, P A -> Q A -> A. End BAZ.
Module BAR_FROM_BAZ (baz : BAZ) : BAR. Import baz. Module foo <: FOO := foo. Import foo. Definition f : forall A, P A -> Q A -> A := g. End BAR_FROM_BAZ.
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.