SUM_CONV : conv
STRUCTURE
listLib
SYNOPSIS
Computes by inference the result of summing the elements of a list.
DESCRIPTION
For any object language list of the form “[x1;x2;...;xn]”, where x1, x2, ..., xn are numeral constants, the result of evaluating 
   SUM_CONV “SUM [x1;x2;...;xn]”
is the theorem 
   |- SUM [x1;x2;...;xn] = n
where n is the numeral constant that denotes the sum of the elements of the list.
EXAMPLE
Evaluating SUM_CONV “SUM [0;1;2;3]” will return the following theorem: 
   |- SUM [0;1;2;3] = 6

FAILURE
SUM_CONV tm fails if tm is not of the form described above.
SEEALSO
FOLDL_CONV, FOLDR_CONV, list_FOLD_CONV
HOL  Kananaskis-13