Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Roqc/theories/Corelib/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 763 B image not shown  

Quelle  dune.disabled   Sprache: unbekannt

 
; For now we use coq_dune to generate the rules here
(coq.theory
 (name Corelib)
 (package rocq-core)
 (synopsis "Rocq's Core Library")
 ; Uncomment this to have dune compile native files in release mode
 ; (mode native)
 (boot)
 (plugins
   rocq-runtime.plugins.ltac
   rocq-runtime.plugins.tauto

   rocq-runtime.plugins.cc
   rocq-runtime.plugins.firstorder

   rocq-runtime.plugins.number_string_notation

   rocq-runtime.plugins.btauto
   rocq-runtime.plugins.rtauto

   rocq-runtime.plugins.ring
   rocq-runtime.plugins.nsatz

   rocq-runtime.plugins.zify
   rocq-runtime.plugins.micromega

   rocq-runtime.plugins.funind

   rocq-runtime.plugins.ssreflect
   rocq-runtime.plugins.derive))

(include_subdirs qualified)

(documentation
 (package rocq-core))

[ Dauer der Verarbeitung: 0.13 Sekunden  (vorverarbeitet)  ]