package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.printing/Ppconstr/index.html

Module PpconstrSource

This module implements pretty-printers for constr_expr syntactic objects and their subcomponents.

Sourcetype flags = {
  1. parentheses : bool;
}
Sourceval current_flags : unit -> flags
Sourceval of_extern_flags : PrintingFlags.Extern.t -> flags
Sourceval of_printing_flags : PrintingFlags.t -> flags
Sourceval pr_tight_coma : unit -> Pp.t
Sourceval pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
Sourceval pr_com_at : int -> Pp.t
Sourceval pr_sep_com : (unit -> Pp.t) -> (Constrexpr.constr_expr -> Pp.t) -> Constrexpr.constr_expr -> Pp.t
Sourceval pr_id : Names.Id.t -> Pp.t
Sourceval pr_qualid : Libnames.qualid -> Pp.t
Sourceval pr_patvar : Pattern.patvar -> Pp.t
Sourceval pr_sort_name_expr : Constrexpr.sort_name_expr -> Pp.t
Sourceval pr_univ_level_expr : Constrexpr.univ_level_expr -> Pp.t
Sourceval pr_sort_expr : Constrexpr.sort_expr -> Pp.t
Sourceval pr_quality_expr : Constrexpr.quality_expr -> Pp.t
Sourceval pr_record : string -> string -> ('a -> Pp.t) -> 'a list -> Pp.t
Sourceval pr_record_body : string -> string -> ('a -> Pp.t) -> (Libnames.qualid * 'a) list -> Pp.t
Sourceval pr_binders : flags:flags -> Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list -> Pp.t
Sourceval pr_constr_pattern_expr : flags:flags -> Environ.env -> Evd.evar_map -> Constrexpr.constr_pattern_expr -> Pp.t
Sourceval pr_lconstr_pattern_expr : flags:flags -> Environ.env -> Evd.evar_map -> Constrexpr.constr_pattern_expr -> Pp.t
Sourceval pr_constr_expr : flags:flags -> Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t
Sourceval pr_lconstr_expr : flags:flags -> Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t
Sourceval pr_cases_pattern_expr : flags:flags -> Constrexpr.cases_pattern_expr -> Pp.t
Sourcetype term_pr = {
  1. pr_constr_expr : flags:flags -> Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t;
  2. pr_lconstr_expr : flags:flags -> Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t;
  3. pr_constr_pattern_expr : flags:flags -> Environ.env -> Evd.evar_map -> Constrexpr.constr_pattern_expr -> Pp.t;
  4. pr_lconstr_pattern_expr : flags:flags -> Environ.env -> Evd.evar_map -> Constrexpr.constr_pattern_expr -> Pp.t;
}
Sourceval set_term_pr : term_pr -> unit
Sourceval default_term_pr : term_pr
Sourceval pr_simpleconstr : flags:flags -> Constrexpr.constr_expr -> Pp.t
Sourceval pr_top : flags:flags -> Constrexpr.constr_expr -> Pp.t
Sourceval modular_constr_pr : flags:flags -> ((unit -> Pp.t) -> int option -> Constrexpr.entry_relative_level -> Constrexpr.constr_expr -> Pp.t) -> (unit -> Pp.t) -> int option -> Constrexpr.entry_relative_level -> Constrexpr.constr_expr -> Pp.t