Ubuntu Online, Fedora Online, Windows online emulator അല്ലെങ്കിൽ MAC OS ഓൺലൈൻ എമുലേറ്റർ എന്നിങ്ങനെയുള്ള ഞങ്ങളുടെ ഒന്നിലധികം സൗജന്യ ഓൺലൈൻ വർക്ക്സ്റ്റേഷനുകളിലൊന്ന് ഉപയോഗിച്ച് OnWorks സൗജന്യ ഹോസ്റ്റിംഗ് ദാതാവിൽ പ്രവർത്തിപ്പിക്കാവുന്ന കമാൻഡ് കോക്ടോപ്പാണിത്.
പട്ടിക:
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 സേവനങ്ങൾ ഉപയോഗിച്ച് കോക്ടോപ്പ് ഓൺലൈനായി ഉപയോഗിക്കുക
