SUM_CONV : conv

- STRUCTURE
- 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 evaluatingis the theorem
SUM_CONV “SUM [x1;x2;...;xn]”

where n is the numeral constant that denotes the sum of the elements of the list.|- SUM [x1;x2;...;xn] = n

- 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

HOL Kananaskis-14