mk_string : string -> term

SYNOPSIS

Constructs object-level string from OCaml string.

DESCRIPTION

mk_string "..." produces the HOL term of type string (which is an abbreviation for char list) corresponding to the OCaml string "...".

FAILURE CONDITIONS

Never fails

EXAMPLE

  # mk_string "hello";;
  val it : term = `"hello"`

  # type_of it;;
  val it : hol_type = `:(char)list`

SEE ALSO

dest_char, dest_list, dest_string, mk_char, mk_list.