NUM_ODD_CONV : conv

SYNOPSIS

Proves whether a natural number numeral is odd.

DESCRIPTION

If n is a numeral (e.g. 0, 1, 2, 3,...), then NUM_ODD_CONV `n` returns one of the theorems:

  |- ODD(n) <=> T

  |- ODD(n) <=> F

according to whether the number denoted by n is odd.

FAILURE CONDITIONS

Fails if applied to a term that is not of the form `ODD n` with n a numeral.

EXAMPLE

  # NUM_ODD_CONV `ODD 123`;;
  val it : thm = |- ODD 123 <=> T

  # NUM_ODD_CONV `ODD 1234`;;
  val it : thm = |- ODD 1234 <=> F

SEE ALSO