sig
  type bound = Free | Bound
  type binding_pattern = Opt.bound array
  val binding_pattern_covers :
    Opt.binding_pattern -> Opt.binding_pattern -> bool
  type mode = InputGround | OutputGround | OutputFree
  type mode_specifier = Opt.mode array
  type discrimination_value = float
  type discrimination_values = Opt.discrimination_value array
  val compute_discrimination_hint :
    Opt.binding_pattern ->
    Opt.discrimination_values -> Opt.discrimination_value
  val make_default_discrimination_hints : int -> Opt.discrimination_values
  type applicability_value = float
  type proof = BuiltinProof | UnknownProof
  type predicate_kind = Edb | Idb | BuiltIn
  type indexargs = WholeTerm | Argument of int | Arguments of int array
  type indextype = HashDt | AlistDt | NoIndex
  type declaration =
      DiscriminationHintsDecl of Opt.discrimination_values
    | IndexDecl of Opt.indextype * Opt.indexargs
    | ModeDecl of Opt.mode_specifier
end