Make (imandra-base.Imandra_interactive_lib.Define_check

Parameters

module _ : Imandra_util_thread.Fut.S

Signature

val top : 
  scope:Opentelemetry.Trace.scope option ->
  ?interrupted:Imandra_util.Switch.t ->
  rproxy:Reasoning_proxy.t ->
  txn:P.Txn.t ->
  Imandra_surface.DB.t ->
  Imandra_surface.Event.t ->
  Imandra_surface.DB_op.t list
  * 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:Reasoning_proxy.t ->
  db:Imandra_surface.DB.t Stdlib.ref ->
  unit ->
  unit