REVERSE_CONV
listLib.REVERSE_CONV : conv
Computes by inference the result of reversing a list.
REVERSE_CONV takes a term tm in the following form:
REVERSE [x0;...xn]
It returns the theorem
|- REVERSE [x0;...xn] = [xn;...x0]
where the right-hand side is the list in the reverse order.
Failure
REVERSE_CONV tm fails if tm is not of the form described above.
Example
Evaluating
REVERSE_CONV “REVERSE [0;1;2;3;4]”;
returns the following theorem:
|- REVERSE [0;1;2;3;4] = [4;3;2;1;0]
See also
listLib.FOLDL_CONV,
listLib.FOLDR_CONV,
listLib.list_FOLD_CONV