dest_char : term -> char

SYNOPSIS

Produces OCaml character corresponding to object-level character.

DESCRIPTION

dest_char t where t is a term of HOL type char, produces the corresponding OCaml character.

FAILURE CONDITIONS

Fails if the term is not of type char

EXAMPLE

  # lhand `"hello"`;;
  val it : term = `ASCII F T T F T F F F`

  # dest_char it;;
  val it : char = 'h'

COMMENTS

There is no particularly convenient parser/printer support for the HOL char type, but when combined into lists they are considered as strings and provided with more intuitive parser/printer support.

SEE ALSO

dest_string, mk_char, mk_string.