package mc2

  1. Overview
  2. Docs
On This Page
  1. Typeclass

Module Term.TCSource

Typeclass

Sourcetype t = tc
Sourceval 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

Sourcetype lazy_tc
Sourceval lazy_from_val : t -> lazy_tc
Sourceval lazy_make : unit -> lazy_tc

Make a new typeclass, without providing the actual functions

Sourceval lazy_get : lazy_tc -> tc

Obtain the underlying typeclass; call only after lazy_complete

Sourceval 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