CHAR_EQ_CONV : term -> thm

SYNOPSIS

Proves equality or inequality of two HOL character literals.

DESCRIPTION

If s and t are two character literal terms in the HOL logic, CHAR_EQ_CONV `s = t` returns:

   |- s = t <=> T       or       |- s = t <=> F

depending on whether the character literals are equal or not equal, respectively.

FAILURE CONDITIONS

CHAR_EQ_CONV tm fails f tm is not of the specified form, an equation between character literals.

EXAMPLE

  # let t = mk_eq(mk_char 'A',mk_char 'A');;
  val t : term = `ASCII F T F F F F F T = ASCII F T F F F F F T`

  # CHAR_EQ_CONV t;;
  val it : thm = |- ASCII F T F F F F F T = ASCII F T F F F F F T <=> T

USES

Performing basic equality reasoning while producing a proof about characters.

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. There is a corresponding proof rule STRING_EQ_CONV for strings.