| products/sources/formale sprachen/Coq/library/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: coqlib.mli Sprache: SMLOriginal von: Coq© |
|
||||||
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \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) *) (************************************************************************) open Util open Names (** Indirection between logical names and global references. This module provides a mechanism to bind “names” to constants and to look up these constants using their names. The two main functions are [register_ref n r] which binds the name [n] to the reference [r] and [lib_ref n] which returns the previously registered reference under name [n]. The first function is meant to be available through the vernacular command [Register r as n], so that plug-ins can refer to a constant without knowing its user-facing name, the precise module path in which it is defined, etc. For instance, [lib_ref "core.eq.type"] returns the proper [GlobRef.t] for the type of the core equality type. *) (** Registers a global reference under the given name. *) val register_ref : string -> GlobRef.t -> unit (** Retrieves the reference bound to the given name (by a previous call to {!register_ref}). Raises an error if no reference is bound to this name. *) val lib_ref : string -> GlobRef.t (** Checks whether a name refers to a registered constant. For any name [n], if [has_ref n] returns [true], [lib_ref n] will succeed. *) val has_ref : string -> bool (** Checks whether a name is bound to a known inductive. *) val check_ind_ref : string -> inductive -> bool (** List of all currently bound names. *) val get_lib_refs : unit -> (string * GlobRef.t) list (* Exceptions to deprecation *) (** {2 For Equality tactics} *) type coq_sigma_data = { proj1 : GlobRef.t; proj2 : GlobRef.t; elim : GlobRef.t; intro : GlobRef.t; typ : GlobRef.t } val build_sigma_set : coq_sigma_data delayed val build_sigma_type : coq_sigma_data delayed val build_sigma : coq_sigma_data delayed type coq_eq_data = { eq : GlobRef.t; ind : GlobRef.t; refl : GlobRef.t; sym : GlobRef.t; trans: GlobRef.t; congr: GlobRef.t } val build_coq_eq_data : coq_eq_data delayed val build_coq_identity_data : coq_eq_data delayed val build_coq_jmeq_data : coq_eq_data delayed (* XXX: Some tactics special case JMeq, they should instead check for the constant, not the module *) (** For tactics/commands requiring vernacular libraries *) val check_required_library : string list -> unit (* Used by obligations *) val datatypes_module_name : string list (* Used by ind_schemes *) val logic_module_name : string list (* Used by tactics *) val jmeq_module_name : string list (*************************************************************************) (** {2 DEPRECATED} *) (*************************************************************************) (** All the functions below are deprecated and should go away in the next coq version ... *) (** [find_reference caller_message [dir;subdir;...] s] returns a global reference to the name dir.subdir.(...).s; the corresponding module must have been required or in the process of being compiled so that it must be used lazily; it raises an anomaly with the given message if not found *) val find_reference : string -> string list -> string -> GlobRef.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** This just prefixes find_reference with Coq... *) val coq_reference : string -> string list -> string -> GlobRef.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Search in several modules (not prefixed by "Coq") *) val gen_reference_in_modules : string->string list list-> string -> GlobRef.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val arith_modules : string list list [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val zarith_base_modules : string list list [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val init_modules : string list list [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** {6 Global references } *) (** Modules *) val logic_module : ModPath.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val logic_type_module : DirPath.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Identity *) val id : Constant.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val type_of_id : Constant.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Natural numbers *) val nat_path : Libnames.full_path [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_nat : GlobRef.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val path_of_O : constructor [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val path_of_S : constructor [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_O : GlobRef.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_S : GlobRef.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Booleans *) val glob_bool : GlobRef.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val path_of_true : constructor [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val path_of_false : constructor [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_true : GlobRef.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_false : GlobRef.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Equality *) val glob_eq : GlobRef.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_identity : GlobRef.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_jmeq : GlobRef.t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** {6 ... } *) (** Constructions and patterns related to Coq initial state are unknown at compile time. Therefore, we can only provide methods to build them at runtime. This is the purpose of the [constr delayed] and [constr_pattern delayed] types. Objects of this time needs to be forced with [delayed_force] to get the actual constr or pattern at runtime. *) type coq_bool_data = { andb : GlobRef.t; andb_prop : GlobRef.t; andb_true_intro : GlobRef.t } val build_bool_type : coq_bool_data delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Non-dependent pairs in Set from Datatypes *) val build_prod : coq_sigma_data delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_eq : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** = [(build_coq_eq_data()).eq] *) val build_coq_eq_refl : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** = [(build_coq_eq_data()).refl] *) val build_coq_eq_sym : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** = [(build_coq_eq_data()).sym] *) val build_coq_f_equal2 : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Data needed for discriminate and injection *) type coq_inversion_data = { inv_eq : GlobRef.t; (** : forall params, args -> Prop *) inv_ind : GlobRef.t; (** : forall params P (H : P params) args, eq params args -> P args *) inv_congr: GlobRef.t (** : forall params B (f:t->B) args, eq params args -> f params = f args *) } val build_coq_inversion_eq_data : coq_inversion_data delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_inversion_identity_data : coq_inversion_data delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_inversion_jmeq_data : coq_inversion_data delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_inversion_eq_true_data : coq_inversion_data delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Specif *) val build_coq_sumbool : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** {6 ... } Connectives The False proposition *) val build_coq_False : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** The True proposition and its unique proof *) val build_coq_True : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_I : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Negation *) val build_coq_not : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Conjunction *) val build_coq_and : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_conj : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_iff : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_iff_left_proj : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_iff_right_proj : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Pairs *) val build_coq_prod : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_pair : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Disjunction *) val build_coq_or : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Existential quantifier *) val build_coq_ex : GlobRef.t delayed [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_eq_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_identity_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_jmeq_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_eq_true_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_existS_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_existT_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_exist_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_not_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_False_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_sumbool_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_sig_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_or_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_iff_ref : GlobRef.t lazy_t [@@ocaml.deprecated "Please use Coqlib.lib_ref"] ¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
