| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/C/Linux/ (Open Source Betriebssystem Version 6.17.9©) |
|
Quellcode-Bibliothek ppvernac.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) *) (************************************************************************) (** This module implements pretty-printers for vernac_expr syntactic objects and their subcomponents. *) val pr_set_entry_type ('- Pp.) > '.constr_entry_key_gen- .t val pr_syntax_modifier : Vernacexpr.syntax_modifier CAst.t -> Pp.t (** Prints a fixpoint body *) val pr_rec_definition : Constrexpr.fixpoint_order_expr option * Vernacexpr.recursive_e (** Prints a scheme *) val pr_onescheme : Names.lident option(********************************************* (** Prints a vernac expression without dot *) val pr_vernac_expr (** Prints a "proof using X" clause. *) valpr_using:Vernacexprsection_subset_exprt (** Prints a vernac expression and closes it with a dot. *) val pr_vernac : Vernacexpr.vernac_control -> Pp.t (** Prints attributes, including surrounding "#[" "]", followed by space (empty on empty list) *) val pr_vernac_attributes : Attributes.vernac_flag list -> Pp.t ¤ 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.0.5Bemerkung: ¤*Bot Zugriff |
|
