NUM_EQ_CONV : conv

SYNOPSIS

Proves equality or inequality of two numerals.

DESCRIPTION

If n and m are two numerals (e.g. 0, 1, 2, 3,...), then NUM_EQ_CONV `n = m` returns:

   |- (n = m) <=> T       or       |- (n = m) <=> F

depending on whether the natural numbers represented by n and m are equal or not equal, respectively.

FAILURE CONDITIONS

NUM_EQ_CONV tm fails if tm is not of the form `n = m`, where n and m are numerals.

EXAMPLE

  # NUM_EQ_CONV `1 = 2`;;
  val it : thm = |- 1 = 2 <=> F

  # NUM_EQ_CONV `12 = 12`;;
  val it : thm = |- 12 = 12 <=> T

USES

Performing basic arithmetic reasoning while producing a proof.

SEE ALSO