Quelle import_mod.v Sprache: Coq

Definition p := 0.
Definition m := 0.

Module Test_Import.
  Module P.
    Definition p := 1.
  End P.

  Module M.
    Import P.
    Definition m := p.
  End M.

  Module N.
    Import M.

    Lemma th0 : p = 0.
      reflexivity.
    Qed.

  End N.

  (* M and P should be closed *)
  Lemma th1 : m = 0 /\ p = 0.
    split; reflexivity.
  Qed.

  Import N.

  (* M and P should still be closed *)
  Lemma th2 : m = 0 /\ p = 0.
    split; reflexivity.
  Qed.
End Test_Import.

(********************************************************************)

Module Test_Export.
  Module P.
    Definition p := 1.
  End P.

  Module M.
    Export P.
    Definition m := p.
  End M.

  Module N.
    Export M.

    Lemma th0 : p = 1.
      reflexivity.
    Qed.

  End N.

  (* M and P should be closed *)
  Lemma th1 : m = 0 /\ p = 0.
    split; reflexivity.
  Qed.

  Import N.

  (* M and P should now be opened *)
  Lemma th2 : m = 1 /\ p = 1.
    split; reflexivity.
  Qed.
End Test_Export.

quality100%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

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.