Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: import_mod.v Sprache: Coq

Original von: 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.

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.