meson_split_limit : int ref
- SYNOPSIS
-
Limit initial case splits before MESON proper is applied.
- DESCRIPTION
-
This is one of several parameters determining the behavior of MESON,
MESON_TAC and related rules and tactics. Before these rules or tactics are
applied, the formula to be proved is often decomposed by splitting, for example
an equivalence p <=> q to two separate implications p ==> q and q ==> p.
This often makes the eventual proof much easier for MESON. On the other hand,
if splitting is applied too many times, it can become inefficient. The value
meson_split_limit (default 8) is the maximum number of times that splitting
can be applied before MESON proper.
- FAILURE CONDITIONS
-
Not applicable.
- USES
-
For users requiring fine control over the algorithms used in MESON's
first-order proof search.
- SEE ALSO
-
meson_brand, meson_chatty, meson_dcutin, meson_depth, meson_prefine,
meson_skew.