type term = Term.tval enum_prop :
?mode:
[ `And
| `Or
| `Neg
| `Quants
| `TF
| `Eq
| `Combinators
| `Full
| `Pragmatic
| `Simple
| `None ] ->
?add_var:bool ->
Term.var Scoped.t ->
enum_cache:Term.Set.t ref ->
signature:Signature.t ->
offset:int ->
(Subst.t * penalty) listGiven a variable of type τ1…τn -> prop, enumerate possible shapes for it
the variable to refine + its scope. Must return prop.
to create fresh variables (should be unused elsewhere)
if `Neg, only tries negation; `None, do nothing; otherwise do all connectives
val pp_pair : pair CCFormat.printerval unif_pairs :
?fuel:int ->
pair list Scoped.t ->
offset:int ->
(pair list * Unif_subst.t * penalty * Subst.Renaming.t) listunif_pairs pairs ~scope_new_vars returns a list of (partial) solutions to the HO unification problem pairs. Each solution is a list of remaining constraints (with the substitution already applied), a substitution, some penalty to influence the search space, and a renaming used for the substitution
val default_fuel : int refDefault amount of fuel for unif_pairs
val enable_norm_subst : bool refIf true, substitutions obtained with unif_pairs are normalized and β-reduced