package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

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

Module `Ppconstr`Source

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

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

Source

val 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

Source

val pr_guard_annot : 
  (Constrexpr.constr_expr -> Pp.t) ->
  Constrexpr.local_binder_expr list ->
  Constrexpr.fixpoint_order_expr option ->
  Pp.t

Sourceval pr_record : string -> string -> ('a -> Pp.t) -> 'a list -> Pp.t

Source

val pr_record_body : 
  string ->
  string ->
  ('a -> Pp.t) ->
  (Libnames.qualid * 'a) list ->
  Pp.t

Source

val pr_binders : 
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.local_binder_expr list ->
  Pp.t

Source

val pr_constr_pattern_expr : 
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_pattern_expr ->
  Pp.t

Source

val pr_lconstr_pattern_expr : 
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_pattern_expr ->
  Pp.t

Source

val pr_constr_expr : 
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_expr ->
  Pp.t

Source

val pr_lconstr_expr : 
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_expr ->
  Pp.t

Sourceval pr_cases_pattern_expr : Constrexpr.cases_pattern_expr -> Pp.t

Source

val pr_constr_expr_n : 
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.entry_relative_level ->
  Constrexpr.constr_expr ->
  Pp.t

Sourcetype term_pr = {

pr_constr_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t;
pr_lconstr_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t;
pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_pattern_expr -> Pp.t;
pr_lconstr_pattern_expr : 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 lsimpleconstr : Constrexpr.entry_relative_level

Sourceval ltop : Constrexpr.entry_relative_level

Sourceval pr_simpleconstr : Constrexpr.constr_expr -> Pp.t

Sourceval pr_top : Constrexpr.constr_expr -> Pp.t

Source

val modular_constr_pr : 
  ((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

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module PpconstrSource

Module `Ppconstr`Source