package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type direction =
  1. | Forward
  2. | Backward
type !'a hint_info_gen = {
  1. hint_priority : int option;
  2. hint_pattern : 'a option;
}
type typeclass = {
  1. cl_univs : Univ.AUContext.t;
  2. cl_impl : Names.GlobRef.t;
  3. cl_context : Names.GlobRef.t option list * Constr.rel_context;
  4. cl_props : Constr.rel_context;
  5. cl_projs : (Names.Name.t * (direction * hint_info) option * Names.Constant.t option) list;
  6. cl_strict : bool;
  7. cl_unique : bool;
}
type instance
val instances : Names.GlobRef.t -> instance list
val typeclasses : unit -> typeclass list
val all_instances : unit -> instance list
val add_class : typeclass -> unit
val new_instance : typeclass -> hint_info -> bool -> Names.GlobRef.t -> instance
val add_instance : instance -> unit
val remove_instance : instance -> unit
val class_info : Names.GlobRef.t -> typeclass
val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass
val instance_impl : instance -> Names.GlobRef.t
val hint_priority : instance -> int option
val is_class : Names.GlobRef.t -> bool
val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list -> EConstr.t option * EConstr.t
type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool
val all_evars : evar_filter
val all_goals : evar_filter
val no_goals : evar_filter
val no_goals_or_obligations : evar_filter
val make_unresolvables : (Evar.t -> bool) -> Evd.evar_map -> Evd.evar_map
val is_class_evar : Evd.evar_map -> Evd.evar_info -> bool
val is_class_type : Evd.evar_map -> EConstr.types -> bool
val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> Environ.env -> Evd.evar_map -> Evd.evar_map
val resolve_one_typeclass : ?unique:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.constr
val set_typeclass_transparency_hook : (Names.evaluable_global_reference -> bool -> bool -> unit) Hook.t
val set_typeclass_transparency : Names.evaluable_global_reference -> bool -> bool -> unit
val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t
val classes_transparent_state : unit -> TransparentState.t
val add_instance_hint_hook : (Globnames.global_reference_or_constr -> Names.GlobRef.t list -> bool -> hint_info -> Decl_kinds.polymorphic -> unit) Hook.t
val remove_instance_hint_hook : (Names.GlobRef.t -> unit) Hook.t
val add_instance_hint : Globnames.global_reference_or_constr -> Names.GlobRef.t list -> bool -> hint_info -> Decl_kinds.polymorphic -> unit
val remove_instance_hint : Names.GlobRef.t -> unit
val solve_all_instances_hook : (Environ.env -> Evd.evar_map -> evar_filter -> bool -> bool -> bool -> Evd.evar_map) Hook.t
val solve_one_instance_hook : (Environ.env -> Evd.evar_map -> EConstr.types -> bool -> Evd.evar_map * EConstr.constr) Hook.t
val declare_instance : ?warn:bool -> hint_info option -> bool -> Names.GlobRef.t -> unit
val build_subclasses : check:bool -> Environ.env -> Evd.evar_map -> Names.GlobRef.t -> hint_info -> (Names.GlobRef.t list * hint_info * Constr.constr) list
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