Module Define.D_client

val top : scope:Opentelemetry.Trace.scope option -> ?interrupted:Imandra_util.Switch.t -> rproxy:Imandra_interactive_lib.Reasoning_proxy.t -> txn:Common_.Define_check_client.P.Txn.t -> Imandra_surface.DB.t -> Imandra_surface.Event.t -> Imandra_surface.DB_op.t list * Common_.Define_check_client.Res.t Imandra_util_thread.Fut.t Imandra_util.Error.result

Check the definition of this event, using the reasoning backend. This involves a network call and possibly a lot of computations on the server side, so it might take quite a while, which is why we return a future.

It also returns a list of additional DB operators that need to be applied in case of success.

This is part of a transaction txn and will be cancelled if txn is.

val done_with_prelude : scope:Opentelemetry.Trace.scope option -> rproxy:Imandra_interactive_lib.Reasoning_proxy.t -> db:Imandra_surface.DB.t Stdlib.ref -> unit -> unit