singleton_of_list : 'a list -> 'a
STRUCTURE
Lib
SYNOPSIS
Turns a single-element list into a singleton.
DESCRIPTION
singleton_of_list [x]
returns
x
.
FAILURE
Fails if applied to a list that is not of length 1.
SEEALSO
pair_of_list
,
triple_of_list
,
quadruple_of_list
HOL
Kananaskis-14