Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
include module type of struct include Ortac_runtime end
type error = Ortac_runtime.error =
| Violated_axiom
| Axiom_failure of {
}
| Violated_invariant of {
term : string;
position : term_kind;
}
| Violated_condition of {
term : string;
term_kind : term_kind;
}
| Specification_failure of {
term : string;
term_kind : term_kind;
exn : exn;
}
| Unexpected_exception of {
}
| Uncaught_checks of {
}
| Unexpected_checks of {
}
val pp_loc : Stdlib.Format.formatter -> location -> unit
val pp_error_report : Stdlib.Format.formatter -> error_report -> unit
exception Error of error_report
module Errors = Ortac_runtime.Errors
exception Partial_function of exn * location
type integer = Ortac_runtime.integer
val string_of_integer : integer -> string
module Gospelstdlib = Ortac_runtime.Gospelstdlib
module Z = Ortac_runtime.Z
type report = {
mod_name : string;
init_sut : string;
ret : expected_result;
cmd : string;
terms : (string * location) list;
}
val report :
string ->
string ->
expected_result ->
string ->
(string * location) list ->
report
module Model : sig ... end
module SUT : sig ... end