এটি হল coqtop কমান্ড যা আমাদের একাধিক বিনামূল্যের অনলাইন ওয়ার্কস্টেশন যেমন উবুন্টু অনলাইন, ফেডোরা অনলাইন, উইন্ডোজ অনলাইন এমুলেটর বা MAC OS অনলাইন এমুলেটর ব্যবহার করে OnWorks ফ্রি হোস্টিং প্রদানকারীতে চালানো যেতে পারে।
কার্যক্রম:
NAME এর
coqtop - Coq প্রুফ সহকারী টপলেভেল সিস্টেম
সাইনোপিসিস
কোকটপ [ অপশন ]
বর্ণনাঃ
কোকটপ ইন্টারেক্টিভ ব্যবহারের জন্য Coq-এর টপলেভেল সিস্টেম। এটা উপর বাক্যাংশ পড়া
স্ট্যান্ডার্ড ইনপুট, এবং স্ট্যান্ডার্ড আউটপুটে ফলাফল প্রিন্ট করে।
Coq এর ব্যাচ-ভিত্তিক ব্যবহারের জন্য, দেখুন coqc(1).
বিকল্প
-হ, --help
সাহায্য আপনাকে coqtop দ্বারা গৃহীত বিকল্পগুলির সম্পূর্ণ তালিকা দেবে৷
-I হয়, --অন্তর্ভুক্ত Dir
ডিরেক্টরি যোগ করুন Dir অন্তর্ভুক্ত পাথ মধ্যে
-R Dir coqdir
recursively ম্যাপ শারীরিক Dir যৌক্তিকভাবে coqdir
-টপ coqdir
শীর্ষ স্তরের নাম সেট করুন coqdir শীর্ষের পরিবর্তে
-ইনপুট স্টেট ফাইলের নাম, -আই ফাইলের নাম
ফাইল থেকে অবস্থা পড়ুন filename.coq
-কোলাহল একটি খালি প্রাথমিক অবস্থা দিয়ে শুরু করুন
-আউটপুট স্টেটফাইলের নাম
ফাইলে রাষ্ট্র লিখুন filename.coq
-লোড-এমএল-অবজেক্ট ফাইলের নাম
ML অবজেক্ট ফাইল লোড করুন ফাইলের নাম
-লোড-এমএল-উৎস ফাইলের নাম
ML ফাইল লোড করুন ফাইলের নাম
-লোড-ভেরনাক-উৎস ফাইলের নাম, -l ফাইলের নাম
Coq ফাইল লোড করুন ফাইলের নাম (ফাইলের নাম লোড করুন।)
-লোড-ভেরনাক-উৎস-ভার্বোস ফাইলের নাম, -lv ফাইলের নাম
শব্দভাবে Coq ফাইল লোড করুন ফাইলের নাম (ভারবোজ ফাইলের নাম লোড করুন।)
-লোড-ভেরনাক-বস্তু ফাইলের নাম
Coq অবজেক্ট ফাইল লোড করুন filename.vo
-প্রয়োজন ফাইলের নাম
Coq অবজেক্ট ফাইল লোড করুন filename.vo এবং এটি আমদানি করুন (ইমপোর্ট ফাইলের নাম প্রয়োজন।)
- কম্পাইল ফাইলের নাম
Coq ফাইল কম্পাইল করুন ফাইলের নাম (উচিত -ব্যাচ )
-সংকলন-ভার্বোস ফাইলের নাম
verbosely Coq ফাইল কম্পাইল ফাইলের নাম (উচিত -ব্যাচ )
-ও Coq এর নেটিভ-কোড সংস্করণ চালান
-বাইট Coq এর বাইটকোড সংস্করণ চালান
-কোথায় Coq এর স্ট্যান্ডার্ড লাইব্রেরি অবস্থান মুদ্রণ করুন এবং প্রস্থান করুন
-v Coq সংস্করণ প্রিন্ট করুন এবং প্রস্থান করুন
-q rcfile লোড করা এড়িয়ে যান
-init-ফাইল ফাইলের নাম
rcfile সেট করুন ফাইলের নাম
-ব্যাচ ব্যাচ মোড (আর্গুমেন্ট পার্স করার পরেই প্রস্থান করে)
-বুট বুট মোড (উচিত -q এবং -ব্যাচ )
- emacs Coq কে বলে যে এটি Emacs এর অধীনে কার্যকর করা হয়
-ডাম্প-গ্লোব ফাইলের নাম
ফাইল f-এ বিশ্বায়ন ডাম্প করুন (এর দ্বারা ব্যবহার করা হবে coqdoc(1) )
-জিওপ্রুফ সহ (হ্যাঁ|না)
(ডি)কোকিডের মধ্যে জিওপ্রুফের জন্য বিশেষ ফাংশন সক্রিয় করতে (ডিফল্ট হল হাঁ )
- অনুমানমূলক - সেট
সেট বাছাই সেট impredicative
-প্রমাণ-লোড করবেন না
মেমরিতে অস্বচ্ছ প্রমাণ লোড করবেন না
-xml XML ফাইলগুলিকে হয় ডিরেক্টরিতে রুট করা অনুক্রমে রপ্তানি করুন
$COQ_XML_LIBRARY_ROOT (যদি সেট থাকে) অথবা stdout (যদি সেট না থাকে)
গুণ
কিছু কৌশল দ্বারা উত্পাদিত প্রমাণ পদের স্পষ্টতা উন্নত করুন
onworks.net পরিষেবা ব্যবহার করে অনলাইনে coqtop ব্যবহার করুন