package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/coq-core.tactics/Ind_tables/index.html

Module Ind_tablesSource

This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand

A scheme is either a "mutual scheme_kind" or an "individual scheme_kind"

Sourcetype mutual
Sourcetype individual
Sourcetype 'a scheme_kind
Sourcetype handle
Sourcetype scheme_dependency =
  1. | SchemeMutualDep of Names.MutInd.t * mutual scheme_kind
  2. | SchemeIndividualDep of Names.inductive * individual scheme_kind
Sourcetype mutual_scheme_object_function = Environ.env -> handle -> Names.MutInd.t -> Constr.constr array Evd.in_evar_universe_context
Sourcetype individual_scheme_object_function = Environ.env -> handle -> Names.inductive -> Constr.constr Evd.in_evar_universe_context

Main functions to register a scheme builder. Note these functions are not safe to be used by plugins as their effects won't be undone on backtracking.

In declare_X_scheme_object key ?suff ?deps f, key is the name of the scheme kind. It must be unique across the Coq process's lifetime. It is used to generate scheme_kind in a marshal-stable way and as the scheme name in Register Scheme.

suff defaults to key, generated schemes which aren't given an explicit name will be named "ind_suff" where "ind" is the inductive's name.

Sourceval declare_mutual_scheme_object : string -> ?suff:string -> ?deps:(Environ.env -> Names.MutInd.t -> scheme_dependency list) -> mutual_scheme_object_function -> mutual scheme_kind
Sourceval declare_individual_scheme_object : string -> ?suff:string -> ?deps:(Environ.env -> Names.inductive -> scheme_dependency list) -> individual_scheme_object_function -> individual scheme_kind
Sourceval is_declared_scheme_object : string -> bool

Is the string used as the name of a scheme_kind?

Sourceval scheme_kind_name : _ scheme_kind -> string

Name of a scheme_kind. Can be used to register with DeclareScheme.

Force generation of a (mutually) scheme with possibly user-level names

Sourceval define_individual_scheme : ?loc:Loc.t -> individual scheme_kind -> Names.Id.t option -> Names.inductive -> unit
Sourcemodule Locmap : sig ... end
Sourceval define_mutual_scheme : ?locmap:Locmap.t -> mutual scheme_kind -> (int * Names.Id.t) list -> Names.MutInd.t -> unit

Main function to retrieve a scheme in the cache or to generate it

Sourceval lookup_scheme : 'a scheme_kind -> Names.inductive -> Names.Constant.t option

Like find_scheme but does not generate a constant on the fly

Sourceval local_lookup_scheme : handle -> 'a scheme_kind -> Names.inductive -> Names.Constant.t option

To be used by scheme-generating functions when looking for a subscheme.

Sourceval pr_scheme_kind : 'a scheme_kind -> Pp.t
Sourceval declare_definition_scheme : (internal:bool -> univs:UState.named_universes_entry -> role:Evd.side_effect_role -> name:Names.Id.t -> ?loc:Loc.t -> Constr.t -> Names.Constant.t * Evd.side_effects) ref