package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val print_sort : Sorts.t -> Pp.t
val pr_sort_family : Sorts.family -> Pp.t
val pr_fix : ('a -> Pp.t) -> ('a, 'a) Constr.pfixpoint -> Pp.t
val push_rel_assum : (Names.Name.t * EConstr.types) -> Environ.env -> Environ.env
val push_rels_assum : (Names.Name.t * Constr.types) list -> Environ.env -> Environ.env
val push_named_rec_types : (Names.Name.t array * Constr.types array * 'a) -> Environ.env -> Environ.env
val lookup_rel_id : Names.Id.t -> ('c, 't) Context.Rel.pt -> int * 'c option * 't
val rel_vect : int -> int -> Constr.constr array
val rel_list : int -> int -> EConstr.constr list
val it_mkProd : EConstr.types -> (Names.Name.t * EConstr.types) list -> EConstr.types
val it_mkLambda : EConstr.constr -> (Names.Name.t * EConstr.types) list -> EConstr.constr
val it_mkProd_or_LetIn : EConstr.types -> EConstr.rel_context -> EConstr.types
val it_mkProd_wo_LetIn : EConstr.types -> EConstr.rel_context -> EConstr.types
val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
val it_mkNamedProd_or_LetIn : EConstr.types -> EConstr.named_context -> EConstr.types
val it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types
val it_mkNamedLambda_or_LetIn : EConstr.constr -> EConstr.named_context -> EConstr.constr
val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
val map_constr_with_binders_left_to_right : Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> EConstr.constr -> EConstr.constr) -> 'a -> EConstr.constr -> EConstr.constr
val map_constr_with_full_binders : Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> EConstr.constr -> EConstr.constr) -> 'a -> EConstr.constr -> EConstr.constr
val fold_constr_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> 'b -> EConstr.constr -> 'b) -> 'a -> 'b -> EConstr.constr -> 'b
val fold_constr_with_full_binders : Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> 'b -> EConstr.constr -> 'b) -> 'a -> 'b -> EConstr.constr -> 'b
val iter_constr_with_full_binders : Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> EConstr.constr -> unit) -> 'a -> EConstr.constr -> unit
val strip_head_cast : Evd.evar_map -> EConstr.constr -> EConstr.constr
val drop_extra_implicit_args : Evd.evar_map -> EConstr.constr -> EConstr.constr
exception Occur
val occur_meta : Evd.evar_map -> EConstr.constr -> bool
val occur_existential : Evd.evar_map -> EConstr.constr -> bool
val occur_meta_or_existential : Evd.evar_map -> EConstr.constr -> bool
val occur_metavariable : Evd.evar_map -> Constr.metavariable -> EConstr.constr -> bool
val occur_evar : Evd.evar_map -> Evar.t -> EConstr.constr -> bool
val occur_var : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool
val occur_var_in_decl : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.named_declaration -> bool
val local_occur_var : Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool
val free_rels : Evd.evar_map -> EConstr.constr -> Int.Set.t
val dependent : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val dependent_no_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val dependent_in_decl : Evd.evar_map -> EConstr.constr -> EConstr.named_declaration -> bool
val count_occurrences : Evd.evar_map -> EConstr.constr -> EConstr.constr -> int
val collect_metas : Evd.evar_map -> EConstr.constr -> int list
val collect_vars : Evd.evar_map -> EConstr.constr -> Names.Id.Set.t
val vars_of_global_reference : Environ.env -> Names.GlobRef.t -> Names.Id.Set.t
type meta_value_map = (Constr.metavariable * Constr.constr) list
val isMetaOf : Evd.evar_map -> Constr.metavariable -> EConstr.constr -> bool
type meta_type_map = (Constr.metavariable * Constr.types) list
val base_sort_cmp : Reduction.conv_pb -> Sorts.t -> Sorts.t -> bool
val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool) -> Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool
val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val eta_reduce_head : Evd.evar_map -> EConstr.constr -> EConstr.constr
val collapse_appl : Evd.evar_map -> EConstr.constr -> EConstr.constr
val prod_applist : Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constr
val prod_applist_assum : Evd.evar_map -> int -> EConstr.constr -> EConstr.constr list -> EConstr.constr
val strip_outer_cast : Evd.evar_map -> EConstr.constr -> EConstr.constr
exception CannotFilter
val decompose_prod_letin : Evd.evar_map -> EConstr.constr -> int * EConstr.rel_context * EConstr.constr
val nb_lam : Evd.evar_map -> EConstr.constr -> int
val nb_prod : Evd.evar_map -> EConstr.constr -> int
val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.constr -> int
val decompose_app_vect : Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr array
val adjust_app_array_size : EConstr.constr -> EConstr.constr array -> EConstr.constr -> EConstr.constr array -> EConstr.constr * EConstr.constr array * EConstr.constr * EConstr.constr array
type names_context = Names.Name.t list
val lookup_name_of_rel : int -> names_context -> Names.Name.t
val lookup_rel_of_name : Names.Id.t -> names_context -> int
val empty_names_context : names_context
val ids_of_rel_context : ('c, 't) Context.Rel.pt -> Names.Id.t list
val ids_of_named_context : ('c, 't) Context.Named.pt -> Names.Id.t list
val ids_of_context : Environ.env -> Names.Id.t list
val names_of_rel_context : Environ.env -> names_context
val env_rel_context_chop : int -> Environ.env -> Environ.env * EConstr.rel_context
val vars_of_env : Environ.env -> Names.Id.Set.t
val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Names.Name.t * 't) list
val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context
val substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context
val smash_rel_context : Constr.rel_context -> Constr.rel_context
val map_rel_context_with_binders : (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt
val fold_named_context_both_sides : ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) -> Constr.named_context -> init:'a -> 'a
val mem_named_context_val : Names.Id.t -> Environ.named_context_val -> bool
val compact_named_context : Constr.named_context -> Constr.compacted_context
val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt
val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt
val clear_named_body : Names.Id.t -> Environ.env -> Environ.env
val global_vars : Environ.env -> Evd.evar_map -> EConstr.constr -> Names.Id.t list
val global_vars_set : Environ.env -> Evd.evar_map -> EConstr.constr -> Names.Id.Set.t
val global_vars_set_of_decl : Environ.env -> Evd.evar_map -> EConstr.named_declaration -> Names.Id.Set.t
val global_app_of_constr : Evd.evar_map -> EConstr.constr -> (Names.GlobRef.t * EConstr.EInstance.t) * EConstr.constr option
val dependency_closure : Environ.env -> Evd.evar_map -> EConstr.named_context -> Names.Id.Set.t -> Names.Id.t list
val is_section_variable : Names.Id.t -> bool
val is_global : Evd.evar_map -> Names.GlobRef.t -> EConstr.constr -> bool
val isGlobalRef : Evd.evar_map -> EConstr.constr -> bool
val is_template_polymorphic : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
val is_Prop : Evd.evar_map -> EConstr.constr -> bool
val is_Set : Evd.evar_map -> EConstr.constr -> bool
val is_Type : Evd.evar_map -> EConstr.constr -> bool
val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid
val on_judgment : ('a -> 'b) -> ('a, 'a) Environ.punsafe_judgment -> ('b, 'b) Environ.punsafe_judgment
val on_judgment_value : ('c -> 'c) -> ('c, 't) Environ.punsafe_judgment -> ('c, 't) Environ.punsafe_judgment
val on_judgment_type : ('t -> 't) -> ('c, 't) Environ.punsafe_judgment -> ('c, 't) Environ.punsafe_judgment
val pr_existential_key : Evd.evar_map -> Evar.t -> Pp.t
val pr_evar_suggested_name : Evar.t -> Evd.evar_map -> Names.Id.t
val pr_evar_info : Evd.evar_info -> Pp.t
val pr_evar_constraints : Evd.evar_map -> Evd.evar_constraint list -> Pp.t
val pr_evar_map : ?with_univs:bool -> int option -> Evd.evar_map -> Pp.t
val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> Evd.evar_info -> bool) -> Evd.evar_map -> Pp.t
val pr_metaset : Evd.Metaset.t -> Pp.t
val pr_evar_universe_context : UState.t -> Pp.t
val pr_evd_level : Evd.evar_map -> Univ.Level.t -> Pp.t
module Internal : sig ... end
val print_constr : EConstr.constr -> Pp.t
  • deprecated This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead
val print_constr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
  • deprecated This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead
val print_rel_context : Environ.env -> Pp.t
  • deprecated This is an internal, debug printer. WARNING, this function is not suitable for plugin code, if you still want to use it then call [Internal.print_rel_context] instead
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