Module `Classes`

Instance declaration

val declare_instance : ?⁠warn:bool -> Environ.env -> Evd.evar_map -> Typeclasses.hint_info option -> bool -> Names.GlobRef.t -> unit: Declares the given global reference as an instance of its type. Does nothing — or emit a “not-a-class” warning if the warn argument is set — when said type is not a registered type class.

val existing_instance : bool -> Libnames.qualid -> Hints.hint_info_expr option -> unit: globality, reference, optional priority and pattern information

val new_instance_interactive : ?⁠global:bool -> poly:bool -> Constrexpr.name_decl -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> ?⁠generalize:bool -> ?⁠tac:unit Proofview.tactic -> ?⁠hook:(Names.GlobRef.t -> unit) -> Hints.hint_info_expr -> (bool * Constrexpr.constr_expr) option -> Names.Id.t * Lemmas.t
val new_instance : ?⁠global:bool -> poly:bool -> Constrexpr.name_decl -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> (bool * Constrexpr.constr_expr) -> ?⁠generalize:bool -> ?⁠hook:(Names.GlobRef.t -> unit) -> Hints.hint_info_expr -> Names.Id.t
val new_instance_program : ?⁠global:bool -> poly:bool -> Constrexpr.name_decl -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> (bool * Constrexpr.constr_expr) option -> ?⁠generalize:bool -> ?⁠hook:(Names.GlobRef.t -> unit) -> Hints.hint_info_expr -> Names.Id.t
val declare_new_instance : ?⁠global:bool -> program_mode:bool -> poly:bool -> Constrexpr.ident_decl -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Hints.hint_info_expr -> unit
val mk_instance : Typeclasses.typeclass -> Typeclasses.hint_info -> bool -> Names.GlobRef.t -> Typeclasses.instance: Low level interface used by Add Morphism, do not use

val add_instance : Typeclasses.instance -> unit
val add_class : Environ.env -> Evd.evar_map -> Typeclasses.typeclass -> unit

val set_typeclass_transparency : Names.evaluable_global_reference -> bool -> bool -> unit