Как избежать необходимости ставить префикс модуля - PullRequest
Новая
       7

Как избежать необходимости ставить префикс модуля

0 голосов
/ 01 июля 2019

До этого я редактировал файл IndProp.v из фондов Программного обеспечения.Но как только я поместил код в отдельный файл, я обнаружил, что для работы команды eqb_neq требуется префикс модуля: Nat.eqb_neq.

Вот код: 

Set Warnings "-notation-overridden,-parsing".
Require Import List.
Import ListNotations.
Require Import PeanoNat.
Local Open Scope nat_scope.

Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).

Example test_nostutter_1: nostutter [3;1;4;1;5;6].
Proof.
  repeat constructor; apply Nat.eqb_neq; auto.
Qed.

Можно ли сказать coq, что я всегда использую здесь модуль Nat, и избавиться от префикса Nat?Как и в C ++, вы можете написать using namespace std;, и вам не нужно будет явно указывать пространство имен перед каждым объектом из него.

1 Ответ

3 голосов
/ 01 июля 2019

Вы можете использовать Import Nat. для этого. Но это может иногда вредить читабельности. Некоторые модули предназначены для использования со своими префиксами, например, stdlib's Vector.

...