Integer Type, Coercions, and Notation #
This file defines the Int
type as well as
- coercions, conversions, and compatibility with numeric literals,
- basic arithmetic operations add/sub/mul/pow,
- a few
Nat
-related operations such asnegOfNat
andsubNatNat
, - relations
<
/≤
/≥
/>
, theNonNeg
property andmin
/max
, - decidability of equality, relations and
NonNeg
.
Division and modulus operations are defined in Init.Data.Int.DivMod.Basic
.
The integers.
This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for Int
that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
GMP). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
- ofNat : Nat → Int
A natural number is an integer.
This constructor covers the non-negative integers (from
0
to∞
). - negSucc : Nat → Int
The negation of the successor of a natural number is an integer.
This constructor covers the negative integers (from
-1
to-∞
).
Instances For
Coercions #
Negation of integers, usually accessed via the -
prefix operator.
This function is overridden by the compiler with an efficient implementation. This definition is the logical model.
Examples:
-(6 : Int) = -6
-(-6 : Int) = 6
(12 : Int).neg = -12
Equations
Instances For
Non-truncating subtraction of two natural numbers.
Examples:
Int.subNatNat 5 2 = 3
Int.subNatNat 2 5 = -3
Int.subNatNat 0 13 = -13
Equations
Instances For
Addition of integers, usually accessed via the +
operator.
This function is overridden by the compiler with an efficient implementation. This definition is the logical model.
Examples:
(7 : Int) + (6 : Int) = 13
(6 : Int) + (-6 : Int) = 0
Equations
Instances For
Multiplication of integers, usually accessed via the *
operator.
This function is overridden by the compiler with an efficient implementation. This definition is the logical model.
Examples:
(63 : Int) * (6 : Int) = 378
(6 : Int) * (-6 : Int) = -36
(7 : Int) * (0 : Int) = 0
Equations
Instances For
Subtraction of integers, usually accessed via the -
operator.
This function is overridden by the compiler with an efficient implementation. This definition is the logical model.
Examples:
(63 : Int) - (6 : Int) = 57
(7 : Int) - (0 : Int) = 7
(0 : Int) - (7 : Int) = -7
Equations
Instances For
Non-strict inequality of integers, usually accessed via the ≤
operator.
a ≤ b
is defined as b - a ≥ 0
, using Int.NonNeg
.
Equations
Instances For
Decides whether two integers are equal. Usually accessed via the DecidableEq Int
instance.
This function is overridden by the compiler with an efficient implementation. This definition is the logical model.
Examples:
show (7 : Int) = (3 : Int) + (4 : Int) by decide
if (6 : Int) = (3 : Int) * (2 : Int) then "yes" else "no" = "yes"
(¬ (6 : Int) = (3 : Int)) = true
Equations
Instances For
Decides whether two integers are equal. Usually accessed via the DecidableEq Int
instance.
This function is overridden by the compiler with an efficient implementation. This definition is the logical model.
Examples:
show (7 : Int) = (3 : Int) + (4 : Int) by decide
if (6 : Int) = (3 : Int) * (2 : Int) then "yes" else "no" = "yes"
(¬ (6 : Int) = (3 : Int)) = true
Equations
The absolute value of an integer is its distance from 0
.
This function is overridden by the compiler with an efficient implementation. This definition is the logical model.
Examples:
Equations
Instances For
sign #
Conversion #
divisibility #
Divisibility of integers. a ∣ b
(typed as \|
) says that
there is some c
such that b = a * c
.
Equations
Powers #
The canonical homomorphism Int → R
. In most use cases, the target type will have a ring structure,
and this homomorphism should be a ring homomorphism.
IntCast
and NatCast
exist to allow different libraries with their own types that can be notated
as natural numbers to have consistent simp
normal forms without needing to create coercion
simplification sets that are aware of all combinations. Libraries should make it easy to work with
IntCast
where possible. For instance, in Mathlib there will be such a homomorphism (and thus an
IntCast R
instance) whenever R
is an additive group with a 1
.
Instances
The canonical homomorphism Int → R
. In most use cases, the target type will have a ring structure,
and this homomorphism should be a ring homomorphism.
IntCast
and NatCast
exist to allow different libraries with their own types that can be notated
as natural numbers to have consistent simp
normal forms without needing to create coercion
simplification sets that are aware of all combinations. Libraries should make it easy to work with
IntCast
where possible. For instance, in Mathlib there will be such a homomorphism (and thus an
IntCast R
instance) whenever R
is an additive group with a 1
.