Quelle common_compile.mli Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* [fatal_error msg] prints msg and exits 1 *)
val fatal_error : Pp.t -> 'a

(* [ensure ext src tgt] checks that, once stripped by ext, both [src] and
   [tgt] have the same basename, and returns [tgt] with the extension.
   [ext] is expected to begin with dot, eg [".v"]. *)
val ensure : ext:string -> src:string -> tgt:string -> string

(* [ensure_exists f] fails if f does not exist *)
val ensure_exists : string -> unit

(* [ensure_exists_with_prefix src tgt src_ext tgt_ext] checks that [src] exists
   (if needed adding the extension) and that [tgt] exists (if needed adding the
   extension) and returns [src] and [tgt] with their respective extensions.
   If [tgt] is [None], then it defaults to [src] (with [tgt_ext] as extension).
   [src_ext] and [tgt_ext] are expected to begin with dot, eg [".v"]. *)
val ensure_exists_with_prefix : src:string -> tgt:string option -> src_ext:string -> tgt_ext:string -> string * string

(* [chop_extension f] is like Filename.chop_extension but fail safe *)
val safe_chop_extension : string -> string

(* [ensure_no_pending_proofs ~filename] checks that no proof or obligation
   is open *)
val ensure_no_pending_proofs : filename:string -> Vernacstate.t -> unit

quality100%

¤ Dauer der Verarbeitung: 0.30 Sekunden (vorverarbeitet) ¤

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.