coqtop - ക്ലൗഡിൽ ഓൺലൈനിൽ

പട്ടിക:

NAME

coqtop - കോക് പ്രൂഫ് അസിസ്റ്റന്റ് ടോപ്ലെവൽ സിസ്റ്റം

സിനോപ്സിസ്

കോക്ടോപ്പ് [ ഓപ്ഷനുകൾ ]

വിവരണം

കോക്ടോപ്പ് സംവേദനാത്മക ഉപയോഗത്തിനുള്ള കോക്കിന്റെ ടോപ്‌ലെവൽ സംവിധാനമാണ്. ഇത് വാക്യങ്ങൾ വായിക്കുന്നു
സ്റ്റാൻഡേർഡ് ഇൻപുട്ട്, സ്റ്റാൻഡേർഡ് ഔട്ട്പുട്ടിൽ ഫലങ്ങൾ പ്രിന്റ് ചെയ്യുന്നു.

Coq-ന്റെ ബാച്ച്-അധിഷ്ഠിത ഉപയോഗത്തിന്, കാണുക coqc(1).

ഓപ്ഷനുകൾ

-h, --സഹായിക്കൂ
സഹായം. coqtop അംഗീകരിച്ച ഓപ്ഷനുകളുടെ പൂർണ്ണമായ ലിസ്റ്റ് നിങ്ങൾക്ക് നൽകും.

-I ആണ്, --ഉൾപ്പെടുന്നു മുതലാളി
ഡയറക്ടറി ചേർക്കുക മുതലാളി ഉൾപ്പെടുന്ന പാതയിൽ

-R മുതലാളി coqdir
ആവർത്തിച്ചുള്ള മാപ്പ് ഫിസിക്കൽ മുതലാളി ലോജിക്കൽ വരെ coqdir

-ടോപ്പ് coqdir
ടോപ്ലെവൽ നാമം ആയി സജ്ജമാക്കുക coqdir ടോപ്പിന് പകരം

-ഇൻപുട്ട് സ്റ്റേറ്റ് ഫയലിന്റെ പേര്, -ഇത് ഫയലിന്റെ പേര്
ഫയലിൽ നിന്ന് അവസ്ഥ വായിക്കുക filename.coq

-ശബ്ദം ഒരു ശൂന്യമായ പ്രാരംഭ അവസ്ഥയിൽ ആരംഭിക്കുക

- outputstateഫയലിന്റെ പേര്
ഫയലിൽ സ്റ്റേറ്റ് എഴുതുക filename.coq

-ലോഡ്-മിലി-ഒബ്ജക്റ്റ് ഫയലിന്റെ പേര്
ML ഒബ്ജക്റ്റ് ഫയൽ ലോഡ് ചെയ്യുക ഫയലിന്റെ പേര്

-load-ml-source ഫയലിന്റെ പേര്
ML ഫയൽ ലോഡ് ചെയ്യുക ഫയലിന്റെ പേര്

-load-vernac-source ഫയലിന്റെ പേര്, -l ഫയലിന്റെ പേര്
Coq ഫയൽ ലോഡ് ചെയ്യുക ഫയൽനാമം.വി (ഫയലിന്റെ പേര് ലോഡ് ചെയ്യുക.)

-load-vernac-source-verbose ഫയലിന്റെ പേര്, -എൽവി ഫയലിന്റെ പേര്
Coq ഫയൽ വാചാലമായി ലോഡ് ചെയ്യുക ഫയൽനാമം.വി (വെർബോസ് ഫയൽനാമം ലോഡ് ചെയ്യുക.)

-load-vernac-object ഫയലിന്റെ പേര്
Coq ഒബ്‌ജക്റ്റ് ഫയൽ ലോഡ് ചെയ്യുക filename.vo

-ആവശ്യമാണ് ഫയലിന്റെ പേര്
Coq ഒബ്‌ജക്റ്റ് ഫയൽ ലോഡ് ചെയ്യുക filename.vo അത് ഇറക്കുമതി ചെയ്യുക (ഇറക്കുമതി ഫയൽനാമം ആവശ്യമാണ്.)

- സമാഹരിക്കുക ഫയലിന്റെ പേര്
Coq ഫയൽ കംപൈൽ ചെയ്യുക ഫയൽനാമം.വി (ധ്വനിപ്പിക്കുന്നു -ബാച്ച് )

-compile-verbose ഫയലിന്റെ പേര്
കോക് ഫയൽ കംപൈൽ ചെയ്യുക ഫയൽനാമം.വി (ധ്വനിപ്പിക്കുന്നു -ബാച്ച് )

-തിരഞ്ഞെടുക്കുക Coq-ന്റെ നേറ്റീവ്-കോഡ് പതിപ്പ് പ്രവർത്തിപ്പിക്കുക

-ബൈറ്റ് Coq-ന്റെ bytecode പതിപ്പ് പ്രവർത്തിപ്പിക്കുക

-എവിടെ Coq ന്റെ സ്റ്റാൻഡേർഡ് ലൈബ്രറി ലൊക്കേഷൻ പ്രിന്റ് ചെയ്ത് പുറത്തുകടക്കുക

-v Coq പതിപ്പ് അച്ചടിച്ച് പുറത്തുകടക്കുക

-q rcfile ലോഡ് ചെയ്യുന്നത് ഒഴിവാക്കുക

-init-file ഫയലിന്റെ പേര്
rcfile സജ്ജമാക്കുക ഫയലിന്റെ പേര്

-ബാച്ച് ബാച്ച് മോഡ് (ആർഗ്യുമെന്റുകൾ പാഴ്സിംഗിന് ശേഷം പുറത്തുകടക്കുന്നു)

-ബൂട്ട് ബൂട്ട് മോഡ് (അതായത് -q ഒപ്പം -ബാച്ച് )

-ഇമാക്സ് ഇമാക്‌സിന് കീഴിൽ ഇത് നടപ്പിലാക്കിയതായി കോക്കിനോട് പറയുന്നു

-ഡമ്പ്-ഗ്ലോബ് ഫയലിന്റെ പേര്
എഫ് ഫയലിൽ ആഗോളവൽക്കരണങ്ങൾ ഡംപ് ചെയ്യുക (ഉപയോഗിക്കുന്നത് coqdoc(1) )

--ജിയോപ്രൂഫ് (അതെ|ഇല്ല)
Coqide-നുള്ളിൽ ജിയോപ്രൂഫിനായി പ്രത്യേക പ്രവർത്തനങ്ങൾ സജീവമാക്കുന്നതിന് (ഡിഫോൾട്ടാണ് അതെ )

-പ്രവചന-സെറ്റ്
ഇംപ്രെഡിക്കേറ്റീവ് സെറ്റ് സോർട്ട്

പ്രൂഫുകൾ ലോഡ് ചെയ്യരുത്
മെമ്മറിയിൽ അതാര്യമായ തെളിവുകൾ ലോഡ് ചെയ്യരുത്

-xml ഡയറക്‌ടറിയിൽ വേരൂന്നിയ ശ്രേണിയിലേക്ക് XML ഫയലുകൾ എക്‌സ്‌പോർട്ടുചെയ്യുക
$COQ_XML_LIBRARY_ROOT (സജ്ജീകരിച്ചിട്ടുണ്ടെങ്കിൽ) അല്ലെങ്കിൽ stdout-ലേക്ക് (സജ്ജീകരിച്ചിട്ടില്ലെങ്കിൽ)

-ഗുണമേന്മയുള്ള
ചില തന്ത്രങ്ങളാൽ നിർമ്മിച്ച പ്രൂഫ് നിബന്ധനകളുടെ വ്യക്തത മെച്ചപ്പെടുത്തുക

onworks.net സേവനങ്ങൾ ഉപയോഗിച്ച് കോക്ടോപ്പ് ഓൺലൈനായി ഉപയോഗിക്കുക