Module Term.TC
Typeclass
type t
= tc
val make : ?init:(Mc2_core__.Solver_types.actions -> Mc2_core__.Solver_types.term -> unit) -> ?update_watches:(Mc2_core__.Solver_types.actions -> Mc2_core__.Solver_types.term -> watch:Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.watch_res) -> ?delete:(Mc2_core__.Solver_types.term -> unit) -> ?subterms:(Mc2_core__.Solver_types.term_view -> (Mc2_core__.Solver_types.term -> unit) -> unit) -> ?eval:(Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.eval_res) -> pp:Mc2_core__.Solver_types.term_view CCFormat.printer -> unit -> t
Make a new typeclass, directly
val lazy_from_val : t -> lazy_tc
val lazy_make : unit -> lazy_tc
Make a new typeclass, without providing the actual functions
val lazy_get : lazy_tc -> tc
Obtain the underlying typeclass; call only after
lazy_complete
val lazy_complete : ?init:(Mc2_core__.Solver_types.actions -> Mc2_core__.Solver_types.term -> unit) -> ?update_watches:(Mc2_core__.Solver_types.actions -> Mc2_core__.Solver_types.term -> watch:Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.watch_res) -> ?delete:(Mc2_core__.Solver_types.term -> unit) -> ?subterms:(Mc2_core__.Solver_types.term_view -> (Mc2_core__.Solver_types.term -> unit) -> unit) -> ?eval:(Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.eval_res) -> pp:Mc2_core__.Solver_types.term_view CCFormat.printer -> lazy_tc -> unit
Now provide functions for this TC.
- raises Failure
if the TC is already defined