如何避免必要加上模块前缀

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.

Nat 前缀?像C++一样,你可以写 using namespace std; 而且不需要在每个对象之前显式地指定名称空间。