(* Variant of #7192 to be tested in a file requiring this file *) (* #7192 is about Print Assumptions not entering implementation of submodules *)
Definition a := True. ModuleType B. Axiom f : Prop. End B. ModuleType C. DeclareModule D : B. End C. Module M7192: C. Module D <: B. Definition f := a. End D. End M7192.
Messung V0.5
¤ Dauer der Verarbeitung: 0.10 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.