package coq

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

See vars.mli for the documentation of the functions below

type instance = t array
type instance_list = t list
type substl = t list
val lift : int -> t -> t
val liftn : int -> int -> t -> t
val substnl : substl -> int -> t -> t
val substl : substl -> t -> t
val subst1 : t -> t -> t
val substnl_decl : substl -> int -> rel_declaration -> rel_declaration
val substl_decl : substl -> rel_declaration -> rel_declaration
val subst1_decl : t -> rel_declaration -> rel_declaration
val replace_vars : (Names.Id.t * t) list -> t -> t
val substn_vars : int -> Names.Id.t list -> t -> t
val subst_vars : Names.Id.t list -> t -> t
val subst_var : Names.Id.t -> t -> t
val noccurn : Evd.evar_map -> int -> t -> bool
val noccur_between : Evd.evar_map -> int -> int -> t -> bool
val closedn : Evd.evar_map -> int -> t -> bool
val closed0 : Evd.evar_map -> t -> bool
val subst_univs_level_constr : Univ.universe_level_subst -> t -> t
val subst_instance_context : Univ.Instance.t -> rel_context -> rel_context
val subst_instance_constr : Univ.Instance.t -> t -> t
val subst_of_rel_context_instance : rel_context -> instance -> substl
val subst_of_rel_context_instance_list : rel_context -> instance_list -> substl
val liftn_rel_context : int -> int -> rel_context -> rel_context
val lift_rel_context : int -> rel_context -> rel_context
val substnl_rel_context : substl -> int -> rel_context -> rel_context
val substl_rel_context : substl -> rel_context -> rel_context
val smash_rel_context : rel_context -> rel_context
val esubst : (int -> 'a -> t) -> 'a Esubst.subs -> t -> t
type substituend
val make_substituend : t -> substituend
val lift_substituend : int -> substituend -> t
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