Module `Declare`Source

This module provides the functions to declare new variables, parameters, constants and inductive types in the global environment. It also updates some accesory tables such as Nametab (name resolution), Impargs, and Notations.

We provide three main entry points:

one-go functions, that will register a constant in one go, suited for non-interactive definitions where the term is given.

two-phase start/save functions which will create an interactive proof, allow its modification using tactics, and saving when complete.

program mode API, that allow to declare a constant with holes, to be fullfilled later.

Note that the API in this file is still in a state of flux, don't hesitate to contact the maintainers if you have any question.

Additionally, this file does contain some low-level functions, marked as such; these functions are unstable and should not be used unless you already know what they are doing.

Sourcemodule Hook : sig ... end

Declaration hooks, to be run when a constant is saved. Use with care, as imperative effects may become not supported in the future.

One-go, non-interactive declaration API

Sourcemodule CInfo : sig ... end

Information for a single top-level named constant

Sourcemodule Info : sig ... end

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

Source

val declare_definition : 
  info:Info.t ->
  cinfo:EConstr.t option CInfo.t ->
  opaque:bool ->
  body:EConstr.t ->
  Evd.evar_map ->
  Names.GlobRef.t

Declares a non-interactive constant; body and types will be normalized w.r.t. the passed evar_map sigma. Universes should be handled properly, including minimization and restriction. Note that sigma is checked for unresolved evars, thus you should be careful not to submit open terms

Source

val declare_assumption : 
  name:Names.Id.t ->
  scope:Locality.locality ->
  hook:Hook.t option ->
  impargs:Impargs.manual_implicits ->
  uctx:UState.t ->
  Entries.parameter_entry ->
  Names.GlobRef.t

Sourcetype lemma_possible_guards = int list list

Source

val declare_mutually_recursive : 
  info:Info.t ->
  cinfo:Constr.t CInfo.t list ->
  opaque:bool ->
  ntns:Vernacexpr.decl_notation list ->
  uctx:UState.t ->
  rec_declaration:Constr.rec_declaration ->
  possible_indexes:lemma_possible_guards option ->
  Names.GlobRef.t list

Declaration of interactive constants

Sourcemodule OblState : sig ... end

save / save_admitted can update obligations state, so we need to expose the state here

Sourcemodule Proof : sig ... end

Declare.Proof.t Construction of constants using interactive proofs.

low-level, internla API, avoid using unless you have special needs

Sourcetype 'a proof_entry

Proof entries represent a proof that has been finished, but still not registered with the kernel.

XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead

Source

val definition_entry : 
  ?opaque:bool ->
  ?using:Names.Id.Set.t ->
  ?inline:bool ->
  ?types:Constr.types ->
  ?univs:Entries.universes_entry ->
  Constr.constr ->
  Evd.side_effects proof_entry

Source

val declare_entry : 
  name:Names.Id.t ->
  scope:Locality.locality ->
  kind:Decls.logical_kind ->
  ?hook:Hook.t ->
  impargs:Impargs.manual_implicits ->
  uctx:UState.t ->
  Evd.side_effects proof_entry ->
  Names.GlobRef.t

XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead

Source

val declare_variable : 
  name:Names.variable ->
  kind:Decls.logical_kind ->
  typ:Constr.types ->
  impl:Glob_term.binding_kind ->
  unit

Declaration of local constructions (Variable/Hypothesis/Local)

Sourcetype 'a constant_entry =

| DefinitionEntry of 'a proof_entry
| ParameterEntry of Entries.parameter_entry
| PrimitiveEntry of Entries.primitive_entry

Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/...

XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead

Source

val prepare_parameter : 
  poly:bool ->
  udecl:UState.universe_decl ->
  types:EConstr.types ->
  Evd.evar_map ->
  Evd.evar_map * Entries.parameter_entry

Source

val declare_constant : 
  ?local:Locality.import_status ->
  name:Names.Id.t ->
  kind:Decls.logical_kind ->
  ?typing_flags:Declarations.typing_flags ->
  Evd.side_effects constant_entry ->
  Names.Constant.t

declare_constant id cd declares a global declaration (constant/parameter) with name id in the current section; it returns the full path of the declaration

XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead

Declaration messages, for internal use

Sourceval definition_message : Names.Id.t -> unit

XXX: Scheduled for removal from public API, do not use

Sourceval assumption_message : Names.Id.t -> unit

Sourceval fixpoint_message : int array option -> Names.Id.t list -> unit

Sourceval check_exists : Names.Id.t -> unit

Source

val build_by_tactic : 
  ?side_eff:bool ->
  Environ.env ->
  uctx:UState.t ->
  poly:bool ->
  typ:EConstr.types ->
  unit Proofview.tactic ->
  Constr.constr
  * Constr.types option
  * Entries.universes_entry
  * bool
  * UState.t

Semantics of this function is a bit dubious, use with care

Program mode API

Coq's Program mode support. This mode extends declarations of constants and fixpoints with Program Definition and Program Fixpoint to support incremental construction of terms using delayed proofs, called "obligations"

The mode also provides facilities for managing and auto-solving sets of obligations.

The basic code flow of programs/obligations is as follows:

add_definition / add_mutual_definitions are called from the respective Program vernacular command interpretation; at this point the only extra work we do is to prepare the new definition d using RetrieveObl, which consists in turning unsolved evars into obligations. d is not sent to the kernel yet, as it is not complete and cannot be typchecked, but saved in a special data-structure. Auto-solving of obligations is tried at this stage (see below)

next_obligation will retrieve the next obligation (RetrieveObl sorts them by topological order) and will try to solve it. When all obligations are solved, the original constant d is grounded and sent to the kernel for addition to the global environment. Auto-solving of obligations is also triggered on obligation completion.

Solving of obligations: Solved obligations are stored as regular global declarations in the global environment, usually with name constant_obligation_number where constant is the original constant and number is the corresponding (internal) number.

Solving an obligation can trigger a bit of a complex cascaded callback path; closing an obligation can indeed allow all other obligations to be closed, which in turn may trigged the declaration of the original constant. Care must be taken, as this can modify Global.env in arbitrarily ways. Current code takes some care to refresh the env in the proper boundaries, but the invariants remain delicate.

Saving of obligations: as open obligations use the regular proof mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason obligations code is split in two: this file, Obligations, taking care of the top-level vernac commands, and Declare, which is called by `Lemmas` to close an obligation proof and eventually to declare the top-level Programed constant.

Sourcemodule Obls : sig ... end

For internal support, do not use

Sourcemodule Internal : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Declare`Source

One-go, non-interactive declaration API

Declaration of interactive constants

low-level, internla API, avoid using unless you have special needs

Program mode API

For internal support, do not use

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module DeclareSource

One-go, non-interactive declaration API

Declaration of interactive constants

low-level, internla API, avoid using unless you have special needs

Program mode API

For internal support, do not use

Module `Declare`Source