(************************************************************************) (* * 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) *) (************************************************************************)
(** This module registers tables for some non-logical informations
associated declarations *)
type assumption_object_kind = Definitional | Logical | Conjectural | Context
(* [assumption_kind]
| Local | Global ------------------------------------ Definitional | Variable | Parameter Logical | Hypothesis | Axiom
*)
(** Kinds *)
type logical_kind =
| IsPrimitive
| IsSymbol
| IsAssumption of assumption_object_kind
| IsDefinition of definition_object_kind
| IsProof of theorem_kind
(** Data associated to section variables and local definitions *)
type variable_data = {
opaque:bool;
kind:logical_kind;
}
let vartab =
Summary.ref (Id.Map.empty : (variable_data*DirPath.t) Id.Map.t) ~name:"VARIABLE"
let secpath () = Lib.current_dirpath true let add_variable_data id o = vartab := Id.Map.add id (o,secpath()) !vartab
let variable_opacity id = let {opaque},_ = Id.Map.find id !vartab in opaque let variable_kind id = let {kind},_ = Id.Map.find id !vartab in kind
let variable_secpath id = let _, dir = Id.Map.find id !vartab in
make_qualid dir id
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.
