meson_split_limit : int ref
Limit initial case splits before MESON proper is applied.
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
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,