package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
Mod_subst
Delta resolver
type delta_resolver

A delta_resolver maps name (constant, inductive, module_path) to canonical name

val empty_delta_resolver : delta_resolver
val add_mp_delta_resolver : Names.ModPath.t -> Names.ModPath.t -> delta_resolver -> delta_resolver
val add_kn_delta_resolver : Names.KerName.t -> Names.KerName.t -> delta_resolver -> delta_resolver
val add_inline_delta_resolver : Names.KerName.t -> (int * Constr.constr Univ.univ_abstracted option) -> delta_resolver -> delta_resolver
val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver

Effect of a delta_resolver on a module path, on a kernel name

Build a constant whose canonical part is obtained via a resolver

val constant_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.Constant.t

Same, but a 2nd resolver is tried if the 1st one had no effect

val constant_of_deltas_kn : delta_resolver -> delta_resolver -> Names.KerName.t -> Names.Constant.t

Same for inductive names

val mind_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.MutInd.t
val inline_of_delta : int option -> delta_resolver -> (int * Names.KerName.t) list

Extract the set of inlined constant in the resolver

Does a delta_resolver contains a mp, a constant, an inductive ?

val mp_in_delta : Names.ModPath.t -> delta_resolver -> bool
val con_in_delta : Names.Constant.t -> delta_resolver -> bool
val mind_in_delta : Names.MutInd.t -> delta_resolver -> bool
Substitution
type substitution
val empty_subst : substitution
val is_empty_subst : substitution -> bool

add_* add arg2/arg1{arg3} to the substitution with no sequential composition. Most often this is not what you want. For sequential composition, try join (map_mbid mp delta) subs *

map_* create a new substitution arg2/arg1{arg3}

sequential composition: substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)

val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver

Apply the substitution on the domain of the resolver

val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver

Apply the substitution on the codomain of the resolver

val subst_dom_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver

subst_mp sub mp guarantees that whenever the result of the substitution is structutally equal mp, it is equal by pointers as well ==

val subst_constructor : substitution -> Names.constructor -> Names.constructor

replace_mp_in_con mp mp' con replaces mp with mp' in con

subst_mps sub c performs the substitution sub on all kernel names appearing in c

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