COQTOP(1)                   General Commands Manual                  COQTOP(1)

نام (NAME)
       coqtop - سامانهٔ تعاملی سطح بالای Coq

خلاصه دستور (SYNOPSIS)
       coqtop [ گزینه‌ها ]

توضیحات (DESCRIPTION)
       coqtop سامانهٔ سطح بالا (toplevel) نرم‌افزار Coq برای استفادهٔ تعاملی است.
       این برنامه عبارت‌ها را از ورودی استاندارد خوانده و نتایج را در خروجی
       استاندارد چاپ می‌کند.  برای استفادهٔ دسته‌ای (غیرتعاملی) از Coq، coqc(1)
       را ببینید.

گزینه‌ها (OPTIONS)
       -h, --help
              راهنما.  فهرست کاملی از گزینه‌های پذیرفته‌شده توسط coqtop را نمایش
              می‌دهد.

       -I dir, --include dir
              افزودن دایرکتوری dir به مسیر جستجو (include path).

       -R dir coqdir
              نگاشت بازگشتی دایرکتوری فیزیکی dir به coqdir منطقی.

       -top coqdir
              تنظیم نام سطح بالا (toplevel) به coqdir به جای Top.

       -nois  شروع با یک وضعیت اولیهٔ خالی.

       -load-ml-source filename
              بارگذاری فایل کد منبع ML به نام filename .

       -load-ml-object filename
              بارگذاری فایل شیء (object) ام‌ال به نام filename .

       -load-vernac-source filename, -l filename
              بارگذاری فایل Coq به نام filename.v .  (دستور .Load filename)

       -load-vernac-source-verbose filename, -lv filename
              بارگذاری پرجزئیات فایل Coq به نام filename.v .  (دستور .Load
              Verbose filename)

       -require lib
              بارگذاری کتابخانهٔ Coq به نام lib .  (دستور .Require lib)

       -require-import lib, -ri lib
              بارگذاری کتابخانهٔ Coq به نام lib و درون‌ریزی (import) آن.  (دستور
              .Require Import lib)

       -require-export lib, -re lib
              بارگذاری کتابخانهٔ Coq به نام lib و درون‌ریزی متعدی (transitive)
              آن.  (دستور .Require Export lib)

       -require-from root lib, -rfrom root lib
              بارگذاری کتابخانهٔ Coq به نام lib .  (دستور .From root Require
              lib)

       -require-import-from root lib, -rifrom root lib
              بارگذاری کتابخانهٔ Coq به نام lib و درون‌ریزی آن.  (دستور .From
              root Require Import lib)

       -require-export-from root lib, -refrom root lib
              بارگذاری کتابخانهٔ Coq به نام lib و درون‌ریزی متعدی آن.  (دستور
              .From root Require Export lib)

       -load-vernac-object lib
              مترادف منسوخ‌شده برای -require.

       -where چاپ مسیر دایرکتوری کتابخانهٔ استاندارد Coq و خروج.

       -v     چاپ نگارش Coq و خروج.

       -q     صرف‌نظر از بارگذاری rcfile (فایل منبع/پیکربندی) در صورت وجود.

       -init-file filename
              تنظیم rcfile به filename .

       -batch حالت دسته‌ای (خروج بلافاصله پس از پردازش آرگومان‌ها).

       -emacs به Coq اطلاع می‌دهد که تحت Emacs اجرا می‌شود.

       -dump-glob filename
              تخلیهٔ سراسری‌سازی‌ها (globalizations) در فایل filename (جهت
              استفاده توسط coqdoc(1)).

       -impredicative-set
              تنظیم ردهٔ (sort) Set به عنوان impredicative.

       -dont-load-proofs
              عدم بارگذاری اثبات‌های مبهم (opaque proofs) در حافظه.

همچنین ببینید (SEE ALSO)
       coqc(1), coq-tex(1), coqdep(1)

       راهنمای مرجع اثبات‌کننده Rocq (The Rocq Prover Reference Manual).

       وب‌گاه Rocq Prover: https://rocq-prover.org

                                                                     COQTOP(1)