package coq-core

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

Module Mod_substSource

Mod_subst
Delta resolver
Sourcetype delta_resolver

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

Sourceval empty_delta_resolver : delta_resolver
Sourceval add_inline_delta_resolver : Names.KerName.t -> (int * Constr.constr UVars.univ_abstracted option) -> delta_resolver -> delta_resolver
Sourceval 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

Sourceval 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

Same for inductive names

Sourceval 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 ?

Sourceval mp_in_delta : Names.ModPath.t -> delta_resolver -> bool
Sourceval con_in_delta : Names.Constant.t -> delta_resolver -> bool
Sourceval mind_in_delta : Names.MutInd.t -> delta_resolver -> bool
Substitution
Sourcetype substitution
Sourceval empty_subst : substitution
Sourceval 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)

Sourceval subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver

Apply the substitution on the domain of the resolver

Sourceval subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver

Apply the substitution on the codomain of the resolver

Sourceval 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 ==

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

Sourceval subst_mps_list : substitution list -> Constr.constr -> Constr.constr
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