Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/doc/plugin_tutorial/tuto1/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 601 B image not shown  

Quellcode-Bibliothek _CoqProject   Sprache: C

 
META.rocq-plugin-tutorial
-R theories Tuto1

# rocq makefile uses -I in 2 ways:
# to tell rocq where the META file is located
-I .
# and to tell the ocaml compiler where previously compiled files are located
# (eg g_tuto1 depends on inspector)
-I src
# in tuto0 with -generate-meta-for-package, the META was generated next to the mlpack
# so -I src did both jobs

theories/Loader.v
theories/Demo.v

src/inspector.mli
src/inspector.ml
src/simple_check.mli
src/simple_check.ml
src/simple_declare.mli
src/simple_declare.ml
src/simple_print.ml
src/simple_print.mli
src/g_tuto1.mlg
src/tuto1_plugin.mlpack

97%


¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.14Bemerkung:  (vorverarbeitet)  ¤

*Bot Zugriff




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.