Module Validate.Response

type rej_reason =
| Res_unknown of {
name : Imandra_surface.Uid.t;
}
| Res_refuted of {
name : Imandra_surface.Uid.t;
model_str_ocaml : string;
model_str_pretty : string;
model_reflect : Imandra_surface.Code_fragment.t option;
}
| Not_a_predicate of {
name : Imandra_surface.Uid.t option;
why : string;
}

Reason why a definition is rejected

val pp_rej_reason : Ppx_deriving_runtime.Format.formatter -> rej_reason -> Ppx_deriving_runtime.unit
val show_rej_reason : rej_reason -> Ppx_deriving_runtime.string
val str_of_reason : long:bool -> rej_reason -> string

Print the reason some definition was rejected.

  • parameter long

    if true, print in long form (including counter-examples).

type on_success = {
event_ops : Imandra_surface.Event.op list;
code_fragments : Imandra_surface.Code_fragment.t list;
}
val pp_on_success : Ppx_deriving_runtime.Format.formatter -> on_success -> Ppx_deriving_runtime.unit
val show_on_success : on_success -> Ppx_deriving_runtime.string
type t = ( on_success, rej_reason ) Stdlib.result
val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string