type term = Term.tval enum_prop :
?mode:[ `Full | `Pragmatic | `Neg | `None | `TF ] ->
Term.var Scoped.t ->
enum_cache:Term.Set.t Stdlib.ref ->
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
Default amount of fuel for unif_pairs
If true, substitutions obtained with unif_pairs are normalized and β-reduced