Q.LIST_REFINE_EXISTS_TAC : term quotation list -> tactic
STRUCTURE
Q
SYNOPSIS
Attacks existential goals, making existential variables more concrete.
LIBRARY
Q
DESCRIPTION
Q.LIST_REFINE_EXISTS_TAC is similar to Q.REFINE_EXISTS_TAC, except it accepts a list of quotations rather than a single one. It further skips quotations of a single variable beginning with an underscore, permitting straightforward refinement of nested existentials.

Note that quotations are parsed right-to-left, so earlier quotations are parsed in the context of later ones.

FAILURE
Fails if passed too many quotations for the current goal. Otherwise fails similarly to Q.REFINE_EXISTS_TAC.
EXAMPLE
  - Q.LIST_REFINE_EXISTS_TAC [`_`,`SUC c`,`_`,`n + m`]
      ([``n = 2``,``c = 5``], ``∃a b c d. a + b = c + d``);
  > val it =
       ([([``n = 2``, ``c = 5``], ``∃a c' m. a + SUC c = c' + (n + m)``)], fn)
       : goal list * validation
USES
Like Q.REFINE_EXISTS_TAC, Q.LIST_REFINE_EXISTS_TAC is useful if it is clear that an existential goal can be solved by a term of particular form, but it is not yet clear exactly what this term will be.

It is particularly useful when refining deeply-nested existentials, or many existentials at once.

COMMENTS
This tactic is also available under the alias bossLib.qrefinel.
SEEALSO
REFINE_EXISTS_TAC, EXISTS_TAC
HOL  Trindemossen-1