Quelle locality_attributes_sections.v
Sprache: Coq
(** This file tests how locality attributes affect usual vernacular commands. PLEASE, when this file fails to compute following a voluntary change in Coq's behaviour, modify accordingly the tables in [sections.rst] and [modules.rst] in [doc/sphinx/language/core].
Also look at the corresponding discussions about locality attributes in the refman (directory doc/sphinx) - For Definition, Lemma, ..., look at language/core/definitions.rst - For Axiom, Conjecture, ..., look at language/core/assumptions.rst - For abbreviations, look at user-extensions/syntax-extensions.rst - For Notations, look at user-extensions/syntax-extensions.rst - For Tactic Notations, look at user-extensions/syntax-extensions.rst - For Ltac, look at proof-engine/ltac.rst - For Canonical Structures, look at language/extensions/canonical.rst - For Hints, look at proofs/automatic-tactics/auto.rst - For Coercions, look at addendum/implicit-coercions.rst - For Ltac2, look at proof-engine/ltac2.rst - For Ltac2 Notations, look at proof-engine/ltac2.rst - For Set, look at language/core/basic.rst
*)
(** This structure is used to test availability or not of a
[Canonical Structure]. *)
Structure PointedType : Type := { Carrier :> Set; point : Carrier }.
(** This HintDb is used to test availability or not of a [Hint] command. *)
Create HintDb plop.
(** ** Tests for sections and visibility attributes *)
(** *** Without attribute (default) *)
Module InSectionDefault.
Section Bar. (* A parameter: *) Parameter (secret : nat). (* An axiom: *) Axiom secret_is_42 : secret = 42. (* A custom tactic: *) Ltac find_secret := rewrite secret_is_42. (* An abbreviation: *) Notation add_42 := (Nat.add 42). (* A tactic notation: *)
Tactic Notation"rfl" := reflexivity. (* A notation: *) Infix"+p" := Nat.add (only parsing, at level 30, right associativity) : nat_scope. (* A lemma: *) Lemma secret_42 : secret = 42. Proof. find_secret. rfl. Qed. (* A Canonical Structure: *)
Canonical natPointed : PointedType := {| Carrier := nat; point := 42 |}. (* A Coercion: *)
Coercion to_nat (b : bool) := if b then 1 else 0. (* A Setting: *) Set Universe Polymorphism. (* A Hint: *) Hint Resolve secret_42 : plop. End Bar.
(* Availability of the parameter *) Check secret. (* Availability of the axiom *) Check secret_is_42. (* Availability of the tactic *)
Fail Print find_secret. (* Availability of the abbreviation *)
Fail Check add_42. (* Availability of the tactic notation *) Lemma plop_i : 2 + 2 = 4. Proof. Fail rfl. Admitted. (* Availability of the notation *)
Fail Check (2 +p 3). (* Availability of the canonical structure *) Check (point nat). (* Availability of the coercion *) Check (true + 2). (* Availability of [Set Universe Polymorphism] *) Definition foo_i@{u} := nat. Check foo_i@{_}. (* Availability of the [Hint] *) Lemma hop_i : secret = 42. Proof.
Fail solve [autowith plop]. Admitted.
End InSectionDefault.
Module InSectionLocal.
Section Bar. (* A parameter: *)
#[local] Parameter (secret : nat). (* An axiom: *)
#[local] Axiom secret_is_42 : secret = 42. (* A custom tactic: *)
#[local] Ltac find_secret := rewrite secret_is_42. (* An abbreviation: *)
#[local] Notation add_42 := (Nat.add 42). (* A tactic notation: *)
#[local]
Tactic Notation"rfl" := reflexivity. (* A notation: *)
#[local] Infix"+p" := Nat.add (only parsing, at level 30, right associativity) : nat_scope. (* A lemma: *)
#[local] Lemma secret_42 : secret = 42. Proof. find_secret. rfl. Qed. (* A Canonical Structure *)
#[local]
Canonical natPointed : PointedType := {| Carrier := nat; point := 42 |}. (* A Coercion *)
#[local]
Coercion to_nat (b : bool) := if b then 1 else 0. (* A Setting *)
#[local] Set Universe Polymorphism. (* A Hint *)
#[local] Hint Resolve secret_42 : plop. End Bar.
(** **** Without importing: *)
(* Availability of the parameter *) Check secret. (* Availability of the axiom *) Check secret_is_42. (* Availability of the tactic *)
Fail Print find_secret. (* Availability of the abbreviation *)
Fail Check add_42. (* Availability of the tactic notation *) Lemma plop_ni : 2 + 2 = 4. Proof. Fail rfl. Admitted. (* Availability of the notation *)
Fail Check (2 +p 3). (* Availability of the canonical structure *)
Fail Check (point nat). (* Availability of the coercion *)
Fail Check (true + 2). (* Availability of [Set Universe Polymorphism] *) Definition foo_ni@{u} := nat.
Fail Check foo_ni@{_}. (* Availability of the [Hint] *) Lemma hop_ni : secret = 42. Proof.
Fail solve [autowith plop]. Admitted. End InSectionLocal.
Module InSectionExport.
Section Bar. (* A parameter: *)
Fail #[export] Parameter (secret : nat). (* An axiom: *)
Fail #[export] Axiom plop : 0 = 0. (* A custom tactic: *)
Fail #[export] Ltac find_secret := reflexivity. (* An abbreviation: *)
Fail #[export] Notation add_42 := (Nat.add 42). (* A tactic notation: *)
Fail #[export]
Tactic Notation"rfl" := reflexivity. (* A notation: *)
Fail #[export] Infix"+p" := Nat.add (only parsing, at level 30, right associativity) : nat_scope. (* A lemma: *)
Fail #[export] Lemma secret_42 : secret = 42. (* A Canonical Structure *)
Fail #[export]
Canonical natPointed : PointedType := {| Carrier := nat; point := 42 |}. (* A Coercion *)
Fail#[export]
Coercion to_nat (b : bool) := if b then 1 else 0. (* A Setting *)
#[export] Set Universe Polymorphism. (* A Hint *) Parameter (secret : nat). Axiom secret_42 : secret = 42.
Fail #[export] Hint Resolve secret_42 : plop. End Bar.
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.
