mk_cons : term -> term -> term

SYNOPSIS

Constructs a CONS pair.

DESCRIPTION

mk_cons `h` `t` returns `CONS h t`.

FAILURE CONDITIONS

Fails if second term is not of list type or if the first term is not of the same type as the elements of the list.

EXAMPLE

  # mk_cons `1` `l:num list`;;
  val it : term = `CONS 1 l`

  # mk_cons `1` `[2;3;4]`;;
  val it : term = `[1; 2; 3; 4]`

SEE ALSO

dest_cons, dest_list, is_cons, is_list, mk_flist, mk_list.