\DOC SNOC_CONV

\TYPE {SNOC_CONV : conv}

\SYNOPSIS
Computes by inference the result of adding an element to the tail end of a list.

\KEYWORDS
conversion, list.

\DESCRIBE
{SNOC_CONV} a term {tm} in the following form:
{
   SNOC x [x0;...xn]
}
\noindent It returns the theorem
{
   |- SNOC x [x0;...xn] = [x0;...xn;x]
}
\noindent 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]";;
}
\noindent 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.

\ENDDOC