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

Quelle  coqlib.mli   Sprache: SML

 
(** Deprecated alias for Rocqlib *)

[@@@ocaml.deprecated "(9.0) Use Rocqlib"]
include module type of struct include Rocqlib end

open Names
open Util

type coq_sigma_data = rocq_sigma_data = {
  proj1 : GlobRef.t;
  proj2 : GlobRef.t;
  elim  : GlobRef.t;
  intro : GlobRef.t;
  typ   : GlobRef.t } [@@ocaml.deprecated "(9.0) Use Rocqlib.rocq_sigma_data"]

type coq_eq_data = rocq_eq_data = {
  eq   : GlobRef.t;
  ind  : GlobRef.t;
  refl : GlobRef.t;
  sym  : GlobRef.t;
  trans: GlobRef.t;
  congr: GlobRef.t } [@@ocaml.deprecated "(9.0) Use Rocqlib.rocq_eq_data"]

val build_coq_eq_data : rocq_eq_data delayed [@@ocaml.deprecated "(9.0) Use Rocqlib.build_rocq_eq_data"]
val build_coq_identity_data : rocq_eq_data delayed [@@ocaml.deprecated "(9.0) Use Rocqlib.build_rocq_identity_data"]
val build_coq_jmeq_data : rocq_eq_data delayed [@@ocaml.deprecated "(9.0) Use Rocqlib.build_rocq_jmeq_data"]

95%


¤ Dauer der Verarbeitung: 0.9 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




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.