Kitaplık nasıl içe aktarılır: Coq.Arith.PeanoNat Coq?

Question

Coq.Arith.PeanoNat (https://coq.inria.fr/library/Coq.Arith.PeanoNat.html) adlı standart kitaplık bölümünü kullanmam gerekir.

Ya tüm arith kütüphane ya da sadece bu modülü ithal denedim, ama her iki durumda da kullanamaz.

Denediğim diğer tüm kitaplıklar gayet iyi çalışıyor. Require Import Bool. yaptığımda derler ve doğru şekilde kullanabilirim. Print Bool. üzerine gelecek biçimde içindeki tüm özelliklerine bakıp alabilir:

Module 
Bool 
:= Struct 
Definition... 
. 
. 
. 
End 

yapmam

ya Require Import Arith.PeanoNat. veya Require Import Arith. bu kadar acil çıktı alın: Ben Coq Print Arith.PeanoNat sorduğumda

[Loading ML file z_syntax_plugin.cmxs ... done] 
[Loading ML file quote_plugin.cmxs ... done] 
[Loading ML file newring_plugin.cmxs ... done] 
<W> Grammar extension: in [tactic:simple_tactic], some rule has been  masked 
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked 
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked 
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked 
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked 

Bu çıktılar: Module Arith := Struct End, boş görünüyor. Kütüphaneden bir şey kullanmaya çalıştığımda, örneğin le_le, boole karşılaştırmaları altında, Error: leb_le not a defined object. standardını aldım Coq ve kütüphaneleri güncelledim ve burada neler olabileceğine dair bir fikrim yok. Bu kütüphane problemini çözmedeki girişinizi takdir ediyorum. Ben Print Arith.PeanoNat çalıştığınızda

Answer 1

, çıkış biraz farklıdır: Ben Module PeanoNat := Struct Module Nat End olsun ve sonra olsa bile leb_le kapsamında değildir Nat.leb_le olduğunu.

(İlgili olması durumunda 8.5beta2 çalıştırıyorum). Ben eğer yanılmıyorsam

Answer 2

, Require bir dosyayı yüklemeye anahtar kelimedir. Import, ad boşluklarını yönetmekle ilgilidir. Genellikle Require Import PeanoNat.'da olduğu gibi birlikte kullanılırlar, ancak gerçekten iki farklı şey yapıyorlar. coq dosyaları (DirName/FileName.vo) Require ile yüklendiğinde FileName.vo içerikleri Module DirName.FileName sarılı ise ... dosyasında tanımlanan End. Bütün olduğunu daha sonra DirName.FileName.Name ile erişilen olarak

, öyle.

Dosyanın kendisi modülleri bunun içinde M olabilir ve M 'ın içeriğine ulaşmak için, tek

Import vb DirName.FileName.ModuleName.Name1 üst seviyeye kadar tüm tanımlamaları almak için kullanılır tuşlamalıdır. Import DirName.FileName.ModuleName yapılarak, Name1 modülü artık en üst düzeye aktarılır ve uzun yol olmadan başvurulabilir. Örnekte

yukarıda, dosya Arith/PeanoNat.vo modülünü Nat tanımlar. Aslında, hepsi bu tanımlar. Yani Require Import Arith.PeanoNat yaparsanız, en üst düzeyde PeanoNat.Nat elde edersiniz. Ve sonra Import PeanoNat.Nat en üst düzeye Nat getirecektir. Require Import PeanoNat.Nat yapamazsınız, çünkü .vo dosyası değil.

Coq bazen tüm yolu belirtmek zorunda kalmadan bir .vo dosyasını bulabilir, böylece Require Import PeanoNat.'u da yapabilirsiniz ve coq dosyayı bulabilir.bunu nerede bulduğunu merak ederse, Locate PeanoNat.

Coq < Require Import PeanoNat. 

Coq < Locate PeanoNat. 
Module Coq.Arith.PeanoNat 

yapmak başka Nat Eğer Require, Yani, değil Import kütüphane yapmak PeanoNat.

Coq < Require Import Nat. 
Warning: Notation _ + _ was already used in scope nat_scope 
Warning: Notation _ * _ was already used in scope nat_scope 
Warning: Notation _ - _ was already used in scope nat_scope 

Coq < Locate Nat. 
Module Coq.Init.Nat 

daha başka bir yerden de kullanılabilir. Tam yol adını kullanmak zorunda kalmamak için Import kullanın. Umarım bu, neler olduğunu ayıklamanıza yardımcı olur.