Module Type.TC
type t
= tc
val make : decide:(Mc2_core__.Solver_types.actions -> Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.value) -> eq:(Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.term) -> mk_state:(unit -> Mc2_core__.Solver_types.decide_state) -> pp:view CCFormat.printer -> unit -> t
Build a typeclass
type lazy_tc
Future typeclass. Acts as a kind of forward declaration that can be used to declare types before actually defining the operations on it
val lazy_make : unit -> lazy_tc
val lazy_from_val : t -> lazy_tc
val lazy_get : lazy_tc -> t
call only after
lazy_complete
val lazy_complete : decide:(Mc2_core__.Solver_types.actions -> Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.value) -> eq:(Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.term) -> mk_state:(unit -> Mc2_core__.Solver_types.decide_state) -> pp:view CCFormat.printer -> lazy_tc -> unit
Set operations of the typeclass, lazily