Module Imandra_interactive.Define

Definition of new symbols

This is the main entrypoint for defining new symbols in Imandra. Typically new symbols come from the parser after the user enters some text into the toplevel interpreter.

first_pass should be true if we're merely defining locally and checking for "redef", false to actually validate

module P = Imandra_protocol
val top : scope:Opentelemetry.Trace.scope option -> ?interrupted:Imandra_util.Switch.t -> txn:P.Txn.t -> db: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
val done_with_prelude : scope:Opentelemetry.Trace.scope option -> db:Imandra_surface.DB.t Stdlib.ref -> unit -> unit