Define (imandra-base.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 Validate_act : sig ... end

module Type : sig ... end

module Modify_state : sig ... end

val top_first_pass : 
  scope:Opentelemetry.Trace.scope option ->
  ?interrupted:Imandra_util.Switch.t ->
  Imandra_surface.Event.t list ->
  unit

val top_second_pass : 
  scope:Opentelemetry.Trace.scope option ->
  ?console_cap:bool ->
  ?interrupted:Imandra_util.Switch.t ->
  Imandra_surface.Event.t list ->
  Validate_act.t Imandra_thread_util.Fut.t

val done_with_prelude : scope:Opentelemetry.Trace.scope option -> unit -> unit