Module `Typeclasses`

type direction = | Forward | Backward
type 'a hint_info_gen = { hint_priority : int option; hint_pattern : 'a option; }
type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
type typeclass = { cl_univs : Univ.AUContext.t; The toplevel universe quantification in which the typeclass lives. In particular, cl_props and cl_context are quantified over it. cl_impl : Names.GlobRef.t; The class implementation: a record parameterized by the context with defs in it or a definition if the class is a singleton. This acts as the class' global identifier. cl_context : Names.GlobRef.t option list * Constr.rel_context; Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The global reference gives a direct link to the class itself. cl_props : Constr.rel_context; Context of definitions and properties on defs, will not be shared cl_projs : (Names.Name.t * (direction * hint_info) option * Names.Constant.t option) list; The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if no name is provided. The int option option indicates subclasses whose hint has the given priority. cl_strict : bool; Whether we use matching or full unification during resolution cl_unique : bool; Whether we can assume that instances are unique, which allows no backtracking and sharing of resolution. }: This module defines type-classes

type instance = { is_class : Names.GlobRef.t; is_info : hint_info; is_global : int option; is_impl : Names.GlobRef.t; }

val instances : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> instance list
val typeclasses : unit -> typeclass list
val all_instances : unit -> instance list
val load_class : typeclass -> unit
val load_instance : instance -> unit
val remove_instance : instance -> unit
val class_info : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> typeclass: raises a UserError if not a class

val dest_class_app : Environ.env -> Evd.evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * Constr.constr list: These raise a UserError if not a class. Caution: the typeclass structures is not instantiated w.r.t. the universe instance. This is done separately by typeclass_univ_instance.

val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass: Get the instantiated typeclass structure for a given universe instance.

val class_of_constr : Environ.env -> Evd.evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * Constr.constr list)) option: Just return None if not a class

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 Stdlib.Lazy.t -> bool: Filter which evars to consider for resolution.

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 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 build_subclasses : check:bool -> Environ.env -> Evd.evar_map -> Names.GlobRef.t -> hint_info -> (Names.GlobRef.t list * hint_info * Constr.constr) list

`cl_univs : Univ.AUContext.t;`	The toplevel universe quantification in which the typeclass lives. In particular, `cl_props` and `cl_context` are quantified over it.
`cl_impl : Names.GlobRef.t;`	The class implementation: a record parameterized by the context with defs in it or a definition if the class is a singleton. This acts as the class' global identifier.
`cl_context : Names.GlobRef.t option list * Constr.rel_context;`	Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The global reference gives a direct link to the class itself.
`cl_props : Constr.rel_context;`	Context of definitions and properties on defs, will not be shared
`cl_projs : (Names.Name.t * (direction * hint_info) option * Names.Constant.t option) list;`	The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if no name is provided. The `int option option` indicates subclasses whose hint has the given priority.
`cl_strict : bool;`	Whether we use matching or full unification during resolution
`cl_unique : bool;`	Whether we can assume that instances are unique, which allows no backtracking and sharing of resolution.