#### Subtypes of integers

Built-in Type
  integers-from(_:integers) <: integers
Alias
  from = integers-from

/*

  `integers-from(M)` is the subtype of integers greater than or equal to `M`.

*/


Built-in Type
  integers-up-to(_:integers) <: integers
Alias
  up-to = integers-up-to

/*

  `integers-up-to(N)` is the subtype of integers less than or equal to `N`.

*/


Type
  bounded-integers(M:integers, N:integers)
    ~> integers-from(M) & integers-up-to(N)
Alias
  bounded-ints = bounded-integers

/*

  `bounded-integers(M,N)` is the subtype of integers from `M` to `N`, inclusive.

*/


Type
  positive-integers ~> integers-from(1)
Alias
  pos-ints = positive-integers


Type
  negative-integers ~> integers-up-to(-1)
Alias
  neg-ints = negative-integers

#### Natural numbers

Type
  natural-numbers ~> integers-from(0)
Alias
  nats = natural-numbers


Built-in Funcon
  natural-successor(N:natural-numbers) : =>natural-numbers
Alias
  nat-succ = natural-successor


Built-in Funcon
  natural-predecessor(_:natural-numbers) : =>natural-numbers?
Alias
  nat-pred = natural-predecessor

Assert

  natural-predecessor(0) == ( )

#### Arithmetic

Built-in Funcon
  integer-add(_:integers*) : =>integers
Alias
  int-add = integer-add


Built-in Funcon
  integer-subtract(_:integers, _:integers) : =>integers
Alias
  int-sub = integer-subtract


Built-in Funcon
  integer-multiply(_:integers*) : =>integers
Alias
  int-mul = integer-multiply


Built-in Funcon
  integer-divide(_:integers, _:integers) : =>integers?
Alias
  int-div = integer-divide

Assert

  integer-divide(_:integers, 0) == ( )

Built-in Funcon
  integer-modulo(_:integers, _:integers) : =>integers?
Alias
  int-mod = integer-modulo

Assert

  integer-modulo(_:integers, 0) == ( )

Built-in Funcon
  integer-power(_:integers, _:natural-numbers) : =>integers
Alias
  int-pow = integer-power

Built-in Funcon
  integer-absolute-value(_:integers) : =>natural-numbers    
Alias
  int-abs = integer-absolute-value

Funcon  integer-negate(N:integers) : =>integers

    ~> integer-subtract(0, N)

Alias
  int-neg = integer-negate

#### Comparison

Built-in Funcon
  integer-is-less(_:integers, _:integers) : =>booleans
Alias
  is-less = integer-is-less


Built-in Funcon
  integer-is-less-or-equal(_:integers, _:integers) : =>booleans
Alias
  is-less-or-equal = integer-is-less-or-equal


Built-in Funcon
  integer-is-greater(_:integers, _:integers) : =>booleans
Alias
  is-greater = integer-is-greater


Built-in Funcon
  integer-is-greater-or-equal(_:integers, _:integers) : =>booleans
Alias
  is-greater-or-equal = integer-is-greater-or-equal

#### Conversion

Built-in Funcon
  binary-natural(_:strings) : =>natural-numbers?
Alias
  binary = binary-natural


Built-in Funcon
  octal-natural(_:strings) : =>natural-numbers?
Alias
  octal = octal-natural


Built-in Funcon
  decimal-natural(_:strings) : =>natural-numbers?
Alias
  decimal = decimal-natural

/*

  Literal natural numbers `N` are equivalent to `decimal-natural"N"`.

*/


Built-in Funcon
  hexadecimal-natural(_:strings) : =>natural-numbers?
Alias
  hexadecimal = hexadecimal-natural


Funcon
  integer-sequence(_:integers, _:integers) : =>integers*

/*

  `integer-sequence(M, N)` is the seqeunce of integers from `M` to `N`,
  except that if `M` is greater than `N`, it is the empty sequence.

*/

Rule

  is-greater(M, N) == false
  ------------------------------------------------
  integer-sequence(M:integers, N:integers)
    ~> (M, integer-sequence(integer-add(M, 1), N))
Rule
  is-greater(M, N) == true
  -----------------------------------------------
  integer-sequence(M:integers, N:integers) ~> ( )