SNOC_CONV : conv

- STRUCTURE
- SYNOPSIS
- Computes by inference the result of adding an element to the tail end of a list.
- DESCRIPTION
- SNOC_CONV takes a term tm in the following form:It returns the theorem
SNOC x [x0;...xn]

where the right-hand side is the list in the canonical form, i.e., constructed with only the constructor CONS.|- SNOC x [x0;...xn] = [x0;...xn;x]

- FAILURE
- SNOC_CONV tm fails if tm is not of the form described above.
- EXAMPLE
- Evaluatingreturns the following theorem:
SNOC_CONV “SNOC 5[0;1;2;3;4]”;

|- SNOC 5[0;1;2;3;4] = [0;1;2;3;4;5]

- SEEALSO

HOL Kananaskis-14