package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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

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

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

Sourceval define_individual_scheme : individual scheme_kind -> Names.Id.t option -> Names.inductive -> unit
Sourceval define_mutual_scheme : 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 -> Constr.t -> Names.Constant.t * Evd.side_effects) ref
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct