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.pretyping/PrintingFlags/Extern/index.html

Module PrintingFlags.ExternSource

Sourcemodule FactorizeEqns : sig ... end
Sourcemodule Records : sig ... end
Sourcetype t = {
  1. use_implicit_types : bool;
  2. records : Records.t;
  3. implicits : bool;
    (*

    When implicits is on then implicits_explicit_args tells how implicit args are printed. If on, implicit args are printed with the form (id:=arg) otherwise arguments are printed normally and the function is prefixed by "@".

    *)
  4. implicits_explicit_args : bool;
  5. implicits_defensive : bool;
  6. coercions : bool;
  7. parentheses : bool;
  8. notations : bool;
  9. raw_literals : bool;
  10. projections : bool;
  11. float : bool;
  12. factorize_eqns : FactorizeEqns.t;
  13. depth : int option;
}
Sourceval make_raw : t -> t
Sourceval current : unit -> t
Sourceval current_ignore_raw : unit -> t