.TH COQTOP 1
.
.SH "نام (NAME)"
coqtop \- سامانهٔ تعاملی سطح بالای Coq
.
.
.SH "خلاصه دستور (SYNOPSIS)"
.B coqtop
[
گزینه‌ها
]
.
.SH "توضیحات (DESCRIPTION)"
.
.B coqtop
سامانهٔ سطح بالا (toplevel) نرم‌افزار Coq برای استفادهٔ تعاملی است.
این برنامه عبارت‌ها را از ورودی استاندارد خوانده و نتایج را در
خروجی استاندارد چاپ می‌کند.
.
برای استفادهٔ دسته‌ای (غیرتعاملی) از Coq،
.BR coqc (1)
را ببینید.
.
.
.SH "گزینه‌ها (OPTIONS)"
.
.TP
.BR \-h , \ \-\-help
راهنما.
فهرست کاملی از گزینه‌های پذیرفته‌شده توسط coqtop را نمایش می‌دهد.
.
.TP
.BI \-I \ dir, \ \-\-include \ dir
افزودن دایرکتوری
.I dir
به مسیر جستجو (include path).
.
.TP
.BI \-R \ dir\ coqdir
نگاشت بازگشتی دایرکتوری فیزیکی
.I dir
به
.I coqdir
منطقی.
.
.TP
.BI \-top \ coqdir
تنظیم نام سطح بالا (toplevel) به
.I coqdir
به جای Top.
.
.TP
.B \-nois
شروع با یک وضعیت اولیهٔ خالی.
.
.TP
.BI \-load\-ml\-source \ filename
بارگذاری فایل کد منبع ML به نام
.I filename .
.
.TP
.BI \-load\-ml\-object \ filename
بارگذاری فایل شیء (object) ام‌ال به نام
.I filename .
.
.TP
.BI \-load\-vernac\-source \ filename, \ \-l \ filename
بارگذاری فایل Coq به نام
.I filename.v .
(دستور .Load filename)
.
.TP
.BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename
بارگذاری پرجزئیات فایل Coq به نام
.I filename.v .
(دستور .Load Verbose filename)
.
.TP
.BI \-require \ lib
بارگذاری کتابخانهٔ Coq به نام
.I lib .
(دستور .Require lib)
.
.TP
.BI \-require-import \ lib, \ \-ri \ lib
بارگذاری کتابخانهٔ Coq به نام
.I lib
و درون‌ریزی (import) آن.
(دستور .Require Import lib)
.
.TP
.BI \-require-export \ lib, \ \-re \ lib
بارگذاری کتابخانهٔ Coq به نام
.I lib
و درون‌ریزی متعدی (transitive) آن.
(دستور .Require Export lib)
.
.TP
.BI \-require-from \ root\ lib, \ \-rfrom \ root\ lib
بارگذاری کتابخانهٔ Coq به نام
.I lib .
(دستور .From root Require lib)
.
.TP
.BI \-require-import-from \ root\ lib, \ \-rifrom \ root\ lib
بارگذاری کتابخانهٔ Coq به نام
.I lib
و درون‌ریزی آن.
(دستور .From root Require Import lib)
.
.TP
.BI \-require-export-from \ root\ lib, \ \-refrom \ root\ lib
بارگذاری کتابخانهٔ Coq به نام
.I lib
و درون‌ریزی متعدی آن.
(دستور .From root Require Export lib)
.
.TP
.BI \-load\-vernac\-object \ lib
مترادف منسوخ‌شده برای
.BR \-require .
.
.TP
.B \-where
چاپ مسیر دایرکتوری کتابخانهٔ استاندارد Coq و خروج.
.
.TP
.B \-v
چاپ نگارش Coq و خروج.
.
.TP
.B \-q
صرف‌نظر از بارگذاری rcfile (فایل منبع/پیکربندی) در صورت وجود.
.
.TP
.BI \-init\-file \ filename
تنظیم rcfile به
.I filename .
.
.TP
.B \-batch
حالت دسته‌ای (خروج بلافاصله پس از پردازش آرگومان‌ها).
.
.TP
.B \-emacs
به Coq اطلاع می‌دهد که تحت Emacs اجرا می‌شود.
.
.TP
.BI \-dump\-glob \ filename
تخلیهٔ سراسری‌سازی‌ها (globalizations) در فایل
.I filename
(جهت استفاده توسط
.BR coqdoc (1)).
.
.TP
.B \-impredicative\-set
تنظیم ردهٔ (sort) Set به عنوان impredicative.
.
.TP
.B \-dont\-load\-proofs
عدم بارگذاری اثبات‌های مبهم (opaque proofs) در حافظه.
.
.SH "همچنین ببینید (SEE ALSO)"
.
.BR coqc (1),
.BR coq-tex (1),
.BR coqdep (1)
.PP
.I
راهنمای مرجع اثبات‌کننده Rocq (The Rocq Prover Reference Manual).
.PP
وب‌گاه Rocq Prover: https://rocq-prover.org