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

type lazy_tc
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