MAP_EVERY : ('a -> tactic) -> 'a list -> tactic
- SYNOPSIS
-
Sequentially applies all tactics given by mapping a function over a list.
- DESCRIPTION
-
When applied to a tactic-producing function f and an operand list
[x1;...;xn], the elements of which have the same type as f's domain type,
MAP_EVERY maps the function f over the list, producing a list of
tactics, then applies these tactics in sequence as in the case of EVERY.
The effect is:
MAP_EVERY f [x1;...;xn] = (f x1) THEN ... THEN (f xn)
- FAILURE CONDITIONS
-
The application of MAP_EVERY to a function and operand list fails iff
the function fails when applied to any element in the list. The
resulting tactic fails iff any of the resulting tactics fails.
- EXAMPLE
-
A convenient way of doing case analysis over several boolean variables is:
MAP_EVERY BOOL_CASES_TAC [`v1:bool`;...;`vn:bool`]
- SEE ALSO
-
EVERY, FIRST, MAP_FIRST, THEN.