अब से पहले मैं सॉफ़्टवेयर फ़ाउंडेशन से 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.

क्या कोक को यह बताना संभव है कि मैं यहां हमेशा नेट मॉड्यूल का उपयोग कर रहा हूं और Nat उपसर्ग से छुटकारा पा रहा हूं? C++ की तरह आप using namespace std; लिख सकते हैं और इसमें से प्रत्येक ऑब्जेक्ट से पहले नेमस्पेस को स्पष्ट रूप से निर्दिष्ट करने की कोई आवश्यकता नहीं होगी।

coq
0
user4035 1 जुलाई 2019, 17:19

1 उत्तर

सबसे बढ़िया उत्तर

ऐसा करने के लिए आप Import Nat. का उपयोग कर सकते हैं। लेकिन यह कभी-कभी पठनीयता को नुकसान पहुंचा सकता है। कुछ मॉड्यूल को उनके उपसर्गों के साथ उपयोग करने के लिए डिज़ाइन किया गया है, उदा। stdlib's Vector.

3
Anton Trunov 1 जुलाई 2019, 17:35