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