Reasoning_proxy (imandra-base.Imandra_interactive_lib.Reasoning

module type CONN = Reasoning_proxy_intf.CONN

module type FRONTEND = Reasoning_proxy_intf.FRONTEND

module type S = Reasoning_proxy_intf.S

type frontend = (module FRONTEND)

type conn = (module CONN)

type t = (module S)

Full proxy with all the functions

val raise_async_error : 
  ( exn -> Stdlib.Printexc.raw_backtrace option -> unit ) Stdlib.ref

val make : conn:(module CONN) -> frontend:(module FRONTEND) -> unit -> t

Create a proxy from the given connection

val dummy_conn : db:Imandra_surface.DB_lock.t -> unit -> (module CONN)

Dummy connection that won't do anything. It reflects updates to the DB into its db parameter.

val make_dummy : 
  db:Imandra_surface.DB_lock.t ->
  frontend:(module FRONTEND) ->
  unit ->
  t

Proxy that uses a dummy connection.