package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

doc/coq-core.vernac/Declare/Info/index.html

Module Declare.InfoSource

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

Sourcetype t
Sourceval make : ?poly:bool -> ?inline:bool -> ?kind:Decls.logical_kind -> ?udecl:UState.universe_decl -> ?scope:Locality.definition_scope -> ?hook:Hook.t -> ?typing_flags:Declarations.typing_flags -> unit -> t

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

OCaml

Innovation. Community. Security.