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-project

Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

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

Sources

rocq-9.2.0.tar.gz

sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.vernac/Declare/Info/index.html

Module `Declare.Info`Source

Information for a declaration, interactive or not, includes parameters shared by mutual constants

Sourcetype t

val make : 
  ?poly:PolyFlags.t ->
  ?inline:bool ->
  ?kind:Decls.logical_kind ->
  ?udecl:UState.universe_decl ->
  ?scope:Locality.definition_scope ->
  ?clearbody:bool ->
  ?hook:Hook.t ->
  ?typing_flags:Declarations.typing_flags ->
  ?user_warns:Globnames.extended_global_reference UserWarn.with_qf ->
  ?ntns:Metasyntax.notation_interpretation_decl list ->
  unit ->
  t

Note that opaque doesn't appear here as it is not known at the start of the proof in the interactive case.