| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/vernac/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 1 kB |
|
Quelle proof_using.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) *) (************************************************************************) (** Utility code for section variables handling in Proof using... *) (** At some point it would be good to make this abstract *) type t = Names.Id.Set.t (** Process a [using] expression in definitions to provide the list of used terms *) val definition_using : Environ.env -> Evd.evar_map -> fixnames:Names.Id.t list (* names of fixpoint occurring recursively, if any *) -> using:Vernacexpr.section_subset_expr -> terms:EConstr.constr list -> t val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit val suggest_constant : Environ.env -> Names.Constant.t -> unit val suggest_variable : Environ.env -> Names.Id.t -> unit val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option val proof_using_opt_name : string list (** For the stm *) val using_from_string : string -> Vernacexpr.section_subset_expr ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28