package mc2

  1. Overview
  2. Docs

Module Type.TCSource

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

Sourcetype 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

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

call only after lazy_complete

Sourceval 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