Module Ortac_runtime_monolith

type location = {
  1. start : Stdlib.Lexing.position;
  2. stop : Stdlib.Lexing.position;
}
type term_kind =
  1. | Check
  2. | Pre
  3. | Post
  4. | XPost
type error =
  1. | Violated_axiom
  2. | Axiom_failure of {
    1. exn : exn;
    }
  3. | Violated_invariant of {
    1. term : string;
    2. position : term_kind;
    }
  4. | Violated_condition of {
    1. term : string;
    2. term_kind : term_kind;
    }
  5. | Specification_failure of {
    1. term : string;
    2. term_kind : term_kind;
    3. exn : exn;
    }
  6. | Unexpected_exception of {
    1. allowed_exn : string list;
    2. exn : exn;
    }
  7. | Uncaught_checks of {
    1. term : string;
    }
  8. | Unexpected_checks of {
    1. terms : string list;
    }
type error_report = {
  1. loc : location;
  2. fun_name : string;
  3. mutable errors : error list;
}
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 : sig ... end
exception Partial_function of exn * location
type integer
val string_of_integer : integer -> string
module Gospelstdlib : sig ... end
module Z : sig ... end
val print_record : string -> (string * PPrint.document) list -> PPrint.document
val print_variant : string -> string -> int -> PPrint.document list -> PPrint.document
val print_tuple : PPrint.document list -> PPrint.document
val constructible_int : (int, int) Monolith.spec
val int : (int, int) Monolith.spec
val positive_int : (int, int) Monolith.spec
val array : ('r, 'c) Monolith.spec -> ('r array, 'c array) Monolith.spec