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
module Gospelstdlib = Ortac_runtime.Gospelstdlib
module Z = Ortac_runtime.Z
type report = {
mod_name : string;
init_sut : string;
ret : (string, STM.res) Stdlib.Either.t;
cmd : string;
terms : (string * location) list;
}