SNOC_CONV : conv
STRUCTURE
listLib
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: 
   SNOC x [x0;...xn]
It returns the theorem 
   |- SNOC x [x0;...xn] = [x0;...xn;x]
where the right-hand side is the list in the canonical form, i.e., constructed with only the constructor CONS.
FAILURE
SNOC_CONV tm fails if tm is not of the form described above.
EXAMPLE
Evaluating 
   SNOC_CONV “SNOC 5[0;1;2;3;4]”;
returns the following theorem: 
   |- SNOC 5[0;1;2;3;4] = [0;1;2;3;4;5]
SEEALSO
FOLDL_CONV, FOLDR_CONV, list_FOLD_CONV
HOL  Trindemossen-1