package mc2

  1. Overview
  2. Docs

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

Lazy builder

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

OCaml

Innovation. Community. Security.