| 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