Quelle PartialImport.v Sprache: Coq

Module M.

  Definition a := 0.
  Definition b := 1.

  Module N.

    Notation c := (a + b).

  End N.

  Inductive even : nat -> Prop :=
  | even_0 : even 0
  | even_S n : odd n -> even (S n)
  with odd : nat -> Set :=
    odd_S n : even n -> odd (S n).

End M.

Module Simple.

  Import M(a).

  Check a.
  Fail Check b.
  Fail Check N.c.

  (* todo output test: this prints a+M.b since the notation isn't imported *)
  Check M.N.c.

  Fail Import M(c).
  Fail Import M(M.b).

  Import M(N.c).
  Check N.c.
  (* interestingly prints N.c (also does with unfiltered Import M) *)

  Import M(even(..)).
  Check even. Check even_0. Check even_S.
  Check even_sind. Check even_ind.
  Fail Check even_rect. (* doesn't exist *)
  Fail Check odd. Check M.odd.
  Fail Check odd_S. Fail Check odd_sind.

End Simple.

Module WithExport.

  Module X.
    Export M(a, N.c).
  End X.

  Import X.
  Check a.
  Check N.c. (* also prints N.c *)
  Fail Check b.

End WithExport.

Module IgnoreLocals.
  Module X.
    Local Definition x := 0.
    Definition y := 1.
  End X.

  Set Warnings "+not-importable".
  Fail Import X(x,y).
  Set Warnings "-not-importable".
  Import X(x,y).
  Check y.
  Fail Check x.
  Check X.x.
End IgnoreLocals.

Module FancyFunctor.
  (* A fancy behaviour with functors, not sure if we want to keep it
     but at least the test will ensure changes are deliberate. *)

  Module Type T.
    Parameter x : nat.
  End T.
  Module X.
    Definition x := 0.
    Definition y := 1.
  End X.

  Module Y.
    Local Definition x := 2.
  End Y.

  Module F(A:T).
    Export A(x).
  End F.
  Module Import M := F X.
  Check x.
  Fail Check y.

  Module N := F Y.
  Set Warnings "+not-importable".
  Fail Import N.
  Set Warnings "-not-importable".
  Import N.
  Check eq_refl : x = 0.

End FancyFunctor.

Require Import Sumbool(sumbool_of_bool).
Check sumbool_of_bool.
Check Sumbool.bool_eq_rec.

Fail Require Sumbool(sumbool_of_bool).
Fail Require Import Sumbool(not_a_real_definition).
Fail Require Import(notations) Sumbool(sumbool_of_bool).

quality99%

¤ Dauer der Verarbeitung: 0.5 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.