NUMSEG_CONV : conv

SYNOPSIS
Expands a specific interval m..n to a set enumeration.

DESCRIPTION
When applied to a term `m..n` (the segment of natural numbers between m and n) for specific numerals m and n, the conversion NUMSEG_CONV returns a theorem of the form |- m..n = {m, ..., n} expressing that segment as a set enumeration.

FAILURE CONDITIONS
Fails unless applied to a term of the form m..n for specific numerals m and n.

EXAMPLE
  # NUMSEG_CONV `7..11`;;
  val it : thm = |- 7..11 = 7, 8, 9, 10, 11

  # NUMSEG_CONV `24..7`;;
  val it : thm = |- 24..7 = 

SEE ALSO
SET_RULE, SET_TAC.