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.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.proofs/Miscprint/index.html

Module MiscprintSource

Printing of intro_pattern

Sourceval pr_intro_pattern : ('a -> Pp.t) -> 'a Tactypes.intro_pattern_expr CAst.t -> Pp.t
Sourceval pr_or_and_intro_pattern : ('a -> Pp.t) -> 'a Tactypes.or_and_intro_pattern_expr -> Pp.t
Sourceval pr_intro_pattern_naming : Namegen.intro_pattern_naming_expr -> Pp.t

Printing of move_location

Sourceval pr_bindings : ('a -> Pp.t) -> ('a -> Pp.t) -> 'a Tactypes.bindings -> Pp.t
Sourceval pr_bindings_no_with : ('a -> Pp.t) -> ('a -> Pp.t) -> 'a Tactypes.bindings -> Pp.t
Sourceval pr_with_bindings : ('a -> Pp.t) -> ('a -> Pp.t) -> ('a * 'a Tactypes.bindings) -> Pp.t