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 (3)

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.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/ssreflect_plugin/Ssreflect_plugin/Ssrprinters/index.html

Module Ssreflect_plugin.SsrprintersSource

Sourceval pr_spc : unit -> Pp.t
Sourceval pr_bar : unit -> Pp.t
Sourceval pr_list : (unit -> Pp.t) -> ('a -> Pp.t) -> 'a list -> Pp.t
Sourceval pp_concat : Pp.t -> ?sep:Pp.t -> Pp.t list -> Pp.t
Sourceval pr_clear : (unit -> Pp.t) -> Ssrast.ssrclear -> Pp.t
Sourceval pr_clear_ne : Ssrast.ssrclear -> Pp.t
Sourceval pr_dir : Ssrast.ssrdir -> Pp.t
Sourceval pr_simpl : Ssrast.ssrsimpl -> Pp.t
Sourceval pr_ast_closure_term : Ssrast.ast_closure_term -> Pp.t
Sourceval pr_view2 : Ssrast.ast_closure_term list -> Pp.t
Sourceval pr_ipat : Ssrast.ssripat -> Pp.t
Sourceval pr_ipats : Ssrast.ssripats -> Pp.t
Sourceval pr_iorpat : Ssrast.ssripatss -> Pp.t
Sourceval pr_block : Ssrast.id_block -> Pp.t
Sourceval pr_hyp : Ssrast.ssrhyp -> Pp.t
Sourceval pr_hyps : Ssrast.ssrhyps -> Pp.t
Sourceval prl_constr_expr : Constrexpr.constr_expr -> Pp.t
Sourceval prl_glob_constr : Glob_term.glob_constr -> Pp.t
Sourceval pr_guarded : (string -> int -> bool) -> ('a -> Pp.t) -> 'a -> Pp.t
Sourceval pr_occ : Ssrast.ssrocc -> Pp.t
Sourceval debug_ssr : CDebug.t