Funcons-beta : Integers.cbs | PRETTY | PDF
Integers
[
Type integers Alias ints
Type integers-from Alias from
Type integers-up-to Alias up-to
Type bounded-integers Alias bounded-ints
Type positive-integers Alias pos-ints
Type negative-integers Alias neg-ints
Type natural-numbers Alias nats
Funcon natural-successor Alias nat-succ
Funcon natural-predecessor Alias nat-pred
Funcon integer-add Alias int-add
Funcon integer-subtract Alias int-sub
Funcon integer-multiply Alias int-mul
Funcon integer-divide Alias int-div
Funcon integer-modulo Alias int-mod
Funcon integer-power Alias int-pow
Funcon integer-absolute-value Alias int-abs
Funcon integer-negate Alias int-neg
Funcon integer-is-less Alias is-less
Funcon integer-is-less-or-equal Alias is-less-or-equal
Funcon integer-is-greater Alias is-greater
Funcon integer-is-greater-or-equal Alias is-greater-or-equal
Funcon binary-natural Alias binary
Funcon octal-natural Alias octal
Funcon decimal-natural Alias decimal
Funcon hexadecimal-natural Alias hexadecimal
Funcon integer-sequence
]Built-in Type
integers
Alias
ints = integersintegers is the type of unbounded integers. Decimal notation is used to
express particular integer values.
Subtypes of integers
Built-in Type
integers-from(_:integers) <: integers
Alias
from = integers-fromintegers-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-tointegers-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-integersbounded-integers(M,N) is the subtype of integers from M to N, inclusive.
Type
positive-integers ~> integers-from(1)
Alias
pos-ints = positive-integersType
negative-integers ~> integers-up-to(-1)
Alias
neg-ints = negative-integersNatural numbers
Type
natural-numbers ~> integers-from(0)
Alias
nats = natural-numbersBuilt-in Funcon
natural-successor(N:natural-numbers) : =>natural-numbers
Alias
nat-succ = natural-successorBuilt-in Funcon
natural-predecessor(_:natural-numbers) : =>natural-numbers?
Alias
nat-pred = natural-predecessorAssert
natural-predecessor(0) == ( )Arithmetic
Built-in Funcon
integer-add(_:integers*) : =>integers
Alias
int-add = integer-addBuilt-in Funcon
integer-subtract(_:integers, _:integers) : =>integers
Alias
int-sub = integer-subtractBuilt-in Funcon
integer-multiply(_:integers*) : =>integers
Alias
int-mul = integer-multiplyBuilt-in Funcon
integer-divide(_:integers, _:integers) : =>integers?
Alias
int-div = integer-divideAssert
integer-divide(_:integers, 0) == ( )Built-in Funcon
integer-modulo(_:integers, _:integers) : =>integers?
Alias
int-mod = integer-moduloAssert
integer-modulo(_:integers, 0) == ( )Built-in Funcon
integer-power(_:integers, _:natural-numbers) : =>integers
Alias
int-pow = integer-powerBuilt-in Funcon
integer-absolute-value(_:integers) : =>natural-numbers
Alias
int-abs = integer-absolute-valueFuncon
integer-negate(N:integers) : =>integers
~> integer-subtract(0, N)
Alias
int-neg = integer-negateComparison
Built-in Funcon
integer-is-less(_:integers, _:integers) : =>booleans
Alias
is-less = integer-is-lessBuilt-in Funcon
integer-is-less-or-equal(_:integers, _:integers) : =>booleans
Alias
is-less-or-equal = integer-is-less-or-equalBuilt-in Funcon
integer-is-greater(_:integers, _:integers) : =>booleans
Alias
is-greater = integer-is-greaterBuilt-in Funcon
integer-is-greater-or-equal(_:integers, _:integers) : =>booleans
Alias
is-greater-or-equal = integer-is-greater-or-equalConversion
Built-in Funcon
binary-natural(_:strings) : =>natural-numbers?
Alias
binary = binary-naturalBuilt-in Funcon
octal-natural(_:strings) : =>natural-numbers?
Alias
octal = octal-naturalBuilt-in Funcon
decimal-natural(_:strings) : =>natural-numbers?
Alias
decimal = decimal-naturalLiteral natural numbers N are equivalent to decimal-natural"N".
Built-in Funcon
hexadecimal-natural(_:strings) : =>natural-numbers?
Alias
hexadecimal = hexadecimal-naturalinteger-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) ~> ( )