mk_flist : term list -> term

SYNOPSIS
Constructs object-level list from nonempty list of terms.

DESCRIPTION
mk_flist [`t1`;...;`tn`] returns `[t1;...;tn]`. The list must be nonempty, since the type could not be inferred for that case. For cases where you may need to construct an empty list, use mk_list.

FAILURE CONDITIONS
Fails if the list is empty or if the types of any elements differ from each other.

EXAMPLE
  # mk_flist(map mk_small_numeral (1--10));;
  val it : term = `[1; 2; 3; 4; 5; 6; 7; 8; 9; 10]`

SEE ALSO
dest_cons, dest_list, is_cons, is_list, mk_cons, mk_list.