package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type delta_resolver
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 * (Univ.AUContext.t * Constr.constr) option) -> delta_resolver -> delta_resolver
val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
val constant_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.Constant.t
val constant_of_deltas_kn : delta_resolver -> delta_resolver -> Names.KerName.t -> Names.Constant.t
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
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
type substitution
val empty_subst : substitution
val is_empty_subst : substitution -> bool
val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver
val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver
val subst_dom_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver
type 'a substituted
val from_val : 'a -> 'a substituted
val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a
val subst_substituted : substitution -> 'a substituted -> 'a substituted
val debug_string_of_subst : substitution -> string
val debug_pr_subst : substitution -> Pp.t
val debug_string_of_delta : delta_resolver -> string
val debug_pr_delta : delta_resolver -> Pp.t
val occur_mbid : Names.MBId.t -> substitution -> bool
val repr_substituted : 'a substituted -> substitution list option * 'a
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