dest_string : term -> string
- SYNOPSIS
-
Produces OCaml string corresponding to object-level string.
- DESCRIPTION
-
dest_string t where t is a literal string in the HOL object logic of type
string (which is an abbreviation for char list), produces the corresponding
OCaml string.
- FAILURE CONDITIONS
-
Fails if the term is not a literal term of type string
- EXAMPLE
-
# dest_string `"HOL"`;;
val it : string = "HOL"
- SEE ALSO
-
dest_char, dest_list, mk_char, mk_list, mk_string.