package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

This files implements typeclasses eauto

val typeclasses_db : string
val set_typeclasses_debug : bool -> unit
val set_typeclasses_depth : int option -> unit
type search_strategy =
  1. | Dfs
  2. | Bfs
val set_typeclasses_strategy : search_strategy -> unit
val typeclasses_eauto : ?only_classes:bool -> ?best_effort:bool -> ?st:TransparentState.t -> ?strategy:search_strategy -> depth:Int.t option -> Hints.hint_db_name list -> unit Proofview.tactic
val head_of_constr : Names.Id.t -> EConstr.constr -> unit Proofview.tactic
val not_evar : EConstr.constr -> unit Proofview.tactic
val is_ground : EConstr.constr -> unit Proofview.tactic
val resolve_tc : EConstr.constr -> unit Proofview.tactic
type solver = {
  1. solver : Environ.env -> Evd.evar_map -> depth:int option -> unique:bool -> best_effort:bool -> goals:Evar.t list -> bool * Evd.evar_map;
}
type condition = Environ.env -> Evd.evar_map -> Evar.Set.t -> bool
type tc_solver = solver * condition

A tc_solver is made of a solver and a condition telling when the the solver should be executed instead of coq's one

val register_solver : name:CString.Map.key -> ?override:bool -> tc_solver -> unit
val activate_solver : name:CString.Map.key -> unit
val deactivate_solver : name:CString.Map.key -> unit
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