Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

ASM_MESON_TAC

mesonLib.ASM_MESON_TAC : thm list -> tactic

Performs first order proof search to prove the goal, using the assumptions and the theorems given.

ASM_MESON_TAC is identical in behaviour to MESON_TAC except that it uses the assumptions of a goal as well as the provided theorems.

Failure

ASM_MESON_TAC fails if it can not find a proof of the goal with depth less than or equal to the mesonLib.max_depth value.

See also

mesonLib.GEN_MESON_TAC, mesonLib.MESON_TAC