Classes (u.dc2732db2fd5639a0cf8e3e92bbaa8d7.coq-core.8.17.1.doc.coq-core.vernac.Classes)

Source

val declare_instance : 
  ?warn:bool ->
  Environ.env ->
  Evd.evar_map ->
  Typeclasses.hint_info option ->
  Hints.hint_locality ->
  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.

Source

val existing_instance : 
  Hints.hint_locality ->
  Libnames.qualid ->
  Vernacexpr.hint_info_expr option ->
  unit

globality, reference, optional priority and pattern information

Source

val new_instance_interactive : 
  locality:Hints.hint_locality ->
  poly:bool ->
  Constrexpr.name_decl ->
  Constrexpr.local_binder_expr list ->
  Constrexpr.constr_expr ->
  ?tac:unit Proofview.tactic ->
  ?hook:(Names.GlobRef.t -> unit) ->
  Vernacexpr.hint_info_expr ->
  (bool * Constrexpr.constr_expr) option ->
  Names.Id.t * Declare.Proof.t

Source

val new_instance : 
  locality:Hints.hint_locality ->
  poly:bool ->
  Constrexpr.name_decl ->
  Constrexpr.local_binder_expr list ->
  Constrexpr.constr_expr ->
  (bool * Constrexpr.constr_expr) ->
  ?hook:(Names.GlobRef.t -> unit) ->
  Vernacexpr.hint_info_expr ->
  Names.Id.t

Source

val new_instance_program : 
  locality:Hints.hint_locality ->
  pm:Declare.OblState.t ->
  poly:bool ->
  Constrexpr.name_decl ->
  Constrexpr.local_binder_expr list ->
  Constrexpr.constr_expr ->
  (bool * Constrexpr.constr_expr) option ->
  ?hook:(Names.GlobRef.t -> unit) ->
  Vernacexpr.hint_info_expr ->
  Declare.OblState.t * Names.Id.t

Source

val declare_new_instance : 
  locality:Hints.hint_locality ->
  program_mode:bool ->
  poly:bool ->
  Constrexpr.ident_decl ->
  Constrexpr.local_binder_expr list ->
  Constrexpr.constr_expr ->
  Vernacexpr.hint_info_expr ->
  unit

Sourceval add_class : Typeclasses.typeclass -> unit

Setting opacity

Source

val set_typeclass_transparency : 
  locality:Hints.hint_locality ->
  Tacred.evaluable_global_reference list ->
  bool ->
  unit

Sourceval tc_transparency_locality : Hints.hint_locality Attributes.attribute

Source

val set_typeclass_transparency_com : 
  locality:Hints.hint_locality ->
  Libnames.qualid list ->
  bool ->
  unit

For generation on names based on classes only

Sourceval id_of_class : Typeclasses.typeclass -> Names.Id.t

Sourceval refine_att : bool Attributes.attribute

Sourceval instance_locality : Hints.hint_locality Attributes.attribute

Sourcemodule Internal : sig ... end