Module `Ind_tables`Source

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 =

| SchemeMutualDep of Names.MutInd.t * mutual scheme_kind
| SchemeIndividualDep of Names.inductive * individual scheme_kind

Source

type mutual_scheme_object_function =
  Environ.env ->
  handle ->
  Names.MutInd.t ->
  Constr.constr array Evd.in_evar_universe_context

Source

type 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.

Source

val declare_mutual_scheme_object : 
  string ->
  ?suff:string ->
  ?deps:(Environ.env -> Names.MutInd.t -> scheme_dependency list) ->
  mutual_scheme_object_function ->
  mutual scheme_kind

Source

val 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

Source

val define_individual_scheme : 
  ?loc:Loc.t ->
  individual scheme_kind ->
  Names.Id.t option ->
  Names.inductive ->
  unit

Sourcemodule Locmap : sig ... end

Source

val define_mutual_scheme : 
  ?locmap:Locmap.t ->
  mutual scheme_kind ->
  (int * Names.Id.t) list ->
  Names.MutInd.t ->
  unit

Source

val find_scheme : 
  'a scheme_kind ->
  Names.inductive ->
  Names.Constant.t Proofview.tactic

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

Source

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

Like find_scheme but does not generate a constant on the fly

Source

val 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

Source

val 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

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Ind_tables`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Ind_tablesSource

Module `Ind_tables`Source