Module Define_check_client.Res

Results of definition/validation

type ctx = {
top_res : Imandra_surface.Top_result.t list;
code : Imandra_surface.Code_fragment.t list;
}
val pp_ctx : Ppx_deriving_runtime.Format.formatter -> ctx -> Ppx_deriving_runtime.unit
val show_ctx : ctx -> Ppx_deriving_runtime.string
type success = {
post_validation_ops : Imandra_surface.DB_op.t list;
}

Operations computed on the reasoning side

type t = {
res : ( success, Imandra_util.Error.t ) Stdlib.result;
ctx : ctx;
}
val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val empty : t
val is_success : t -> bool
val raise_if_err : t -> unit

If res is Error e, raises e as an exception.