12.4. 固定精度整数型（Fixed-Precision Integer Types）🔗

Lean の標準ライブラリには一般的な固定長整数型が含まれています。形式化と証明の観点において、これらの型は適切なサイズのビットベクタを包んだラッパです；このラッパによって、例えば算術演算の正しい実装が適用されることが保証されます。コンパイルされたコードでは、これらの型は効率的な表現になります：コンパイラは他の基本的な型と同様に、これらの型を特別にサポートしています。

12.4.1. 論理モデル（Logical Model）

固定長整数は符号なしと符号ありのどちらも可能です。さらに、5種類のサイズがあります；8 ・ 16 ・ 32 ・ 64 ビットおよび現在のアーキテクチャのワードサイズと同じものです。論理モデルでは、符号なし整数は適切な幅の BitVec をラップした構造体です。符号付き整数は対応する符号なし整数をラップし、2 の補数表現を使用します。

12.4.1.1. 符号なし（Unsigned）

🔗structure
USize : Type

A USize is an unsigned integer with the size of a word for the platform's architecture.

For example, if running on a 32-bit machine, USize is equivalent to UInt32. Or on a 64-bit machine, UInt64.

Constructor

USize.mk

Fields

toBitVec : BitVec System.Platform.numBits

Unpack a USize as a BitVec System.Platform.numBits. This function is overridden with a native implementation.

🔗structure
UInt8 : Type

The type of unsigned 8-bit integers. This type has special support in the compiler to make it actually 8 bits rather than wrapping a Nat.

Constructor

UInt8.mk

Fields

toBitVec : BitVec 8

Unpack a UInt8 as a BitVec 8. This function is overridden with a native implementation.

🔗structure
UInt16 : Type

The type of unsigned 16-bit integers. This type has special support in the compiler to make it actually 16 bits rather than wrapping a Nat.

Constructor

UInt16.mk

Fields

toBitVec : BitVec 16

Unpack a UInt16 as a BitVec 16. This function is overridden with a native implementation.

🔗structure
UInt32 : Type

The type of unsigned 32-bit integers. This type has special support in the compiler to make it actually 32 bits rather than wrapping a Nat.

Constructor

UInt32.mk

Fields

toBitVec : BitVec 32

Unpack a UInt32 as a `BitVec 32. This function is overridden with a native implementation.

🔗structure
UInt64 : Type

The type of unsigned 64-bit integers. This type has special support in the compiler to make it actually 64 bits rather than wrapping a Nat.

Constructor

UInt64.mk

Fields

toBitVec : BitVec 64

Unpack a UInt64 as a BitVec 64. This function is overridden with a native implementation.

12.4.1.2. 符号あり（Signed）

🔗structure
ISize : Type

A ISize is a signed integer with the size of a word for the platform's architecture.

For example, if running on a 32-bit machine, ISize is equivalent to Int32. Or on a 64-bit machine, Int64.

Constructor

ISize.mk

Fields

toUSize : USize

Obtain the USize that is 2's complement equivalent to the ISize.

🔗structure
Int8 : Type

The type of signed 8-bit integers. This type has special support in the compiler to make it actually 8 bits rather than wrapping a Nat.

Constructor

Int8.mk

Fields

toUInt8 : UInt8

Obtain the UInt8 that is 2's complement equivalent to the Int8.

🔗structure
Int16 : Type

The type of signed 16-bit integers. This type has special support in the compiler to make it actually 16 bits rather than wrapping a Nat.

Constructor

Int16.mk

Fields

toUInt16 : UInt16

Obtain the UInt16 that is 2's complement equivalent to the Int16.

🔗structure
Int32 : Type

The type of signed 32-bit integers. This type has special support in the compiler to make it actually 32 bits rather than wrapping a Nat.

Constructor

Int32.mk

Fields

toUInt32 : UInt32

Obtain the UInt32 that is 2's complement equivalent to the Int32.

🔗structure
Int64 : Type

The type of signed 64-bit integers. This type has special support in the compiler to make it actually 64 bits rather than wrapping a Nat.

Constructor

Int64.mk

Fields

toUInt64 : UInt64

Obtain the UInt64 that is 2's complement equivalent to the Int64.

12.4.2. ランタイム表現（Run-Time Representation）

コンパイルされたコードでは、プラットフォームのポインタサイズより1ビット小さいサイズに収まる固定長整数型は、追加の割り当てやインダイレクション無しでボックス化解除されたものとして表現されます。 Int8 ・ UInt8 ・ Int16 ・ UInt16 は必ずこれに含まれます。64ビットのアーキテクチャでは、 Int32 と UInt32 もボックス化解除されます。

プラットフォームのポインタ型のビット数以上の固定長整数型は Nat と同じ方法で表現されます：十分に小さい場合はボックス化解除され、大きい場合はヒープに割り当てられた数値として表現されます。 Int64 ・ UInt64 ・ ISize ・ USize は必ずこの方法で表現され、32ビットのアーキテクチャでは Int32 と UInt32 も同様です。

12.4.3. 構文（Syntax）

すべての固定長整数型は OfNat インスタンスを持っており、式とパターンのコンテキストの両方で数値をリテラルとして使用することができます。符号あり型はさらに Neg インスタンスを持っており、マイナスを適用することができます。

固定長リテラル

Lean では、 OfNat インスタンスを持つ型に対して10進数と16進数の両方のリテラルを使用することができます。この例では、マスクの定義にリテラル表記を使用しています。

structure Permissions where readable : Bool writable : Bool executable : Bool def Permissions.encode (p : Permissions) : UInt8 := let r := if p.readable then 0x01 else 0 let w := if p.writable then 0x02 else 0 let x := if p.executable then 0x04 else 0 r ||| w ||| x def Permissions.decode (i : UInt8) : Permissions := ⟨i &&& 0x01 ≠ 0, i &&& 0x02 ≠ 0, i &&& 0x04 ≠ 0⟩

型の精度をオーバーフローするリテラルは、その精度の剰余として解釈されます。符号あり型では、基礎となる2の補数表現に従って解釈されます。

オーバーフローした固定長リテラル

以下の文は全て真です：

example : (255 : UInt8) = 255 := ⊢ 255 = 255 All goals completed! 🐙 example : (256 : UInt8) = 0 := ⊢ 256 = 0 All goals completed! 🐙 example : (257 : UInt8) = 1 := ⊢ 257 = 1 All goals completed! 🐙 example : (0x7f : Int8) = 127 := ⊢ 127 = 127 All goals completed! 🐙 example : (0x8f : Int8) = -113 := ⊢ 143 = -113 All goals completed! 🐙 example : (0xff : Int8) = -1 := ⊢ 255 = -1 All goals completed! 🐙

12.4.4. API リファレンス（API Reference）

12.4.4.1. サイズ（Sizes）

各固定長整数には サイズ があり、これはその型が表現できることを示す個別の数値です。これは C の sizeof 演算子とは同等ではなく、型が占めるバイト数を決定するものです。

🔗def
USize.size : Nat

The size of type USize, that is, 2^System.Platform.numBits.

🔗def
ISize.size : Nat

The size of type ISize, that is, 2^System.Platform.numBits.

🔗def
UInt8.size : Nat

The size of type UInt8, that is, 2^8 = 256.

🔗def
Int8.size : Nat

The size of type Int8, that is, 2^8 = 256.

🔗def
UInt16.size : Nat

The size of type UInt16, that is, 2^16 = 65536.

🔗def
Int16.size : Nat

The size of type Int16, that is, 2^16 = 65536.

🔗def
UInt32.size : Nat

The size of type UInt32, that is, 2^32 = 4294967296.

🔗def
Int32.size : Nat

The size of type Int32, that is, 2^32 = 4294967296.

🔗def
UInt64.size : Nat

The size of type UInt64, that is, 2^64 = 18446744073709551616.

🔗def
Int64.size : Nat

The size of type Int64, that is, 2^64 = 18446744073709551616.

12.4.4.2. 変換（Conversions）

12.4.4.2.1. Int との相互変換（To and From Int）

🔗def
ISize.toInt (i : ISize) : Int
🔗def
Int8.toInt (i : Int8) : Int
🔗def
Int16.toInt (i : Int16) : Int
🔗def
Int32.toInt (i : Int32) : Int
🔗def
Int64.toInt (i : Int64) : Int
🔗def
ISize.ofInt (i : Int) : ISize
🔗def
Int8.ofInt (i : Int) : Int8
🔗def
Int16.ofInt (i : Int) : Int16
🔗def
Int32.ofInt (i : Int) : Int32
🔗def
Int64.ofInt (i : Int) : Int64

12.4.4.2.2. Nat との相互変換（To and From Nat）

🔗def
USize.ofNat (n : Nat) : USize
🔗def
ISize.ofNat (n : Nat) : ISize
🔗def
UInt8.ofNat (n : Nat) : UInt8
🔗def
Int8.ofNat (n : Nat) : Int8
🔗def
UInt16.ofNat (n : Nat) : UInt16
🔗def
Int16.ofNat (n : Nat) : Int16
🔗def
UInt32.ofNat (n : Nat) : UInt32
🔗def
UInt32.ofNat' (n : Nat) (h : n < UInt32.size)
    : UInt32
🔗def
UInt32.ofNatTruncate (n : Nat) : UInt32

Converts the given natural number to UInt32, but returns 2^32 - 1 for natural numbers >= 2^32.

🔗def
Int32.ofNat (n : Nat) : Int32
🔗def
UInt64.ofNat (n : Nat) : UInt64
🔗def
Int64.ofNat (n : Nat) : Int64
🔗def
USize.ofNat32 (n : Nat) (h : n < 4294967296)
    : USize

Upcast a Nat less than 2^32 to a USize. This is lossless because USize.size is either 2^32 or 2^64. This function is overridden with a native implementation.

🔗def
USize.ofNatCore (n : Nat) (h : n < USize.size)
    : USize

Pack a Nat less than USize.size into a USize. This function is overridden with a native implementation.

🔗def
UInt8.ofNatCore (n : Nat) (h : n < UInt8.size)
    : UInt8

Pack a Nat less than 2^8 into a UInt8. This function is overridden with a native implementation.

🔗def
UInt16.ofNatCore (n : Nat) (h : n < UInt16.size)
    : UInt16

Pack a Nat less than 2^16 into a UInt16. This function is overridden with a native implementation.

🔗def
UInt32.ofNatCore (n : Nat) (h : n < UInt32.size)
    : UInt32

Pack a Nat less than 2^32 into a UInt32. This function is overridden with a native implementation.

🔗def
UInt64.ofNatCore (n : Nat) (h : n < UInt64.size)
    : UInt64

Pack a Nat less than 2^64 into a UInt64. This function is overridden with a native implementation.

🔗def
USize.toNat (n : USize) : Nat
🔗def
ISize.toNat (i : ISize) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

🔗def
UInt8.toNat (n : UInt8) : Nat
🔗def
Int8.toNat (i : Int8) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

🔗def
UInt16.toNat (n : UInt16) : Nat
🔗def
Int16.toNat (i : Int16) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

🔗def
UInt32.toNat (n : UInt32) : Nat

Unpack a UInt32 as a Nat. This function is overridden with a native implementation.

🔗def
Int32.toNat (i : Int32) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

🔗def
UInt64.toNat (n : UInt64) : Nat
🔗def
Int64.toNat (i : Int64) : Nat

This function has the same behavior as Int.toNat for negative numbers. If you want to obtain the 2's complement representation use toBitVec.

12.4.4.2.3. その他の固定長整数への変換（To Other Fixed-Width Integers）

🔗def
Int32.toISize (a : Int32) : ISize

Upcast Int32 to ISize. This function is losless as ISize is either Int32 or Int64.

🔗def
Int64.toISize (a : Int64) : ISize
🔗def
ISize.toInt32 (a : ISize) : Int32
🔗def
Int8.toInt32 (a : Int8) : Int32
🔗def
Int16.toInt32 (a : Int16) : Int32
🔗def
ISize.toInt64 (a : ISize) : Int64

Upcast ISize to Int64. This function is losless as ISize is either Int32 or Int64.

🔗def
USize.toUInt8 (a : USize) : UInt8
🔗def
UInt16.toUInt8 (a : UInt16) : UInt8
🔗def
Int16.toInt8 (a : Int16) : Int8
🔗def
UInt32.toUInt8 (a : UInt32) : UInt8
🔗def
Int32.toInt8 (a : Int32) : Int8
🔗def
UInt64.toUInt8 (a : UInt64) : UInt8
🔗def
Int64.toInt8 (a : Int64) : Int8
🔗def
USize.toUInt16 (a : USize) : UInt16
🔗def
UInt8.toUInt16 (a : UInt8) : UInt16
🔗def
Int8.toInt16 (a : Int8) : Int16
🔗def
UInt32.toUInt16 (a : UInt32) : UInt16
🔗def
Int32.toInt16 (a : Int32) : Int16
🔗def
UInt64.toUInt16 (a : UInt64) : UInt16
🔗def
Int64.toInt16 (a : Int64) : Int16
🔗def
USize.toUInt32 (a : USize) : UInt32
🔗def
UInt8.toUInt32 (a : UInt8) : UInt32
🔗def
Int8.toInt32 (a : Int8) : Int32
🔗def
UInt16.toUInt32 (a : UInt16) : UInt32
🔗def
Int16.toInt32 (a : Int16) : Int32
🔗def
UInt64.toUInt32 (a : UInt64) : UInt32
🔗def
Int64.toInt32 (a : Int64) : Int32
🔗def
USize.toUInt64 (a : USize) : UInt64

Upcast a USize to a UInt64. This is lossless because USize.size is either 2^32 or 2^64. This function is overridden with a native implementation.

🔗def
UInt8.toUInt64 (a : UInt8) : UInt64
🔗def
Int8.toInt64 (a : Int8) : Int64
🔗def
UInt16.toUInt64 (a : UInt16) : UInt64
🔗def
Int16.toInt64 (a : Int16) : Int64
🔗def
UInt32.toUInt64 (a : UInt32) : UInt64
🔗def
Int32.toInt64 (a : Int32) : Int64
🔗def
UInt8.toUSize (a : UInt8) : USize
🔗def
UInt16.toUSize (a : UInt16) : USize
🔗def
UInt32.toUSize (a : UInt32) : USize
🔗def
UInt64.toUSize (a : UInt64) : USize

Converts a UInt64 to a USize by reducing modulo USize.size.

12.4.4.2.4. 浮動小数点への変換（To Floating-Point Numbers）

🔗opaque
UInt64.toFloat (n : UInt64) : Float
🔗opaque
UInt64.toFloat32 (n : UInt64) : Float32

12.4.4.2.5. ビットベクタへの変換（To Bitvectors）

🔗def
ISize.toBitVec (x : ISize)
    : BitVec System.Platform.numBits

Obtain the BitVec that contains the 2's complement representation of the ISize.

🔗def
Int8.toBitVec (x : Int8) : BitVec 8

Obtain the BitVec that contains the 2's complement representation of the Int8.

🔗def
Int16.toBitVec (x : Int16) : BitVec 16

Obtain the BitVec that contains the 2's complement representation of the Int16.

🔗def
Int32.toBitVec (x : Int32) : BitVec 32

Obtain the BitVec that contains the 2's complement representation of the Int32.

🔗def
Int64.toBitVec (x : Int64) : BitVec 64

Obtain the BitVec that contains the 2's complement representation of the Int64.

12.4.4.2.6. 有限な値への変換（To Finite Numbers）

🔗def
USize.val (x : USize) : Fin USize.size
🔗def
UInt8.val (x : UInt8) : Fin UInt8.size
🔗def
UInt16.val (x : UInt16) : Fin UInt16.size
🔗def
UInt32.val (x : UInt32) : Fin UInt32.size
🔗def
UInt64.val (x : UInt64) : Fin UInt64.size
🔗def
USize.repr (n : USize) : String

12.4.4.2.7. 文字型への変換（To Characters）

Char 型は UInt32 のラッパであり、ラップされた整数が Unicode のコードポイントを表すことを証明する必要があります。この述語は UInt32 API の一部です。

🔗def
UInt32.isValidChar (n : UInt32) : Prop

A UInt32 denotes a valid unicode codepoint if it is less than 0x110000, and it is also not a "surrogate" character (the range 0xd800 to 0xdfff inclusive).

12.4.4.3. 比較（Comparisons）🔗

本節の演算子が名前で呼び出されることはほとんどありません。通常、固定長整数に対する比較演算は、対応する関係についての決定性を使用する必要があり、等号型 Eq と LE ・ LT のインスタンスで実装されているものから構成されます。

🔗def
USize.le (a b : USize) : Prop
🔗def
ISize.le (a b : ISize) : Prop
🔗def
UInt8.le (a b : UInt8) : Prop
🔗def
Int8.le (a b : Int8) : Prop
🔗def
UInt16.le (a b : UInt16) : Prop
🔗def
Int16.le (a b : Int16) : Prop

{docstring UInt32.le}

🔗def
Int32.le (a b : Int32) : Prop
🔗def
UInt64.le (a b : UInt64) : Prop
🔗def
Int64.le (a b : Int64) : Prop
🔗def
USize.lt (a b : USize) : Prop
🔗def
ISize.lt (a b : ISize) : Prop
🔗def
UInt8.lt (a b : UInt8) : Prop
🔗def
Int8.lt (a b : Int8) : Prop
🔗def
UInt16.lt (a b : UInt16) : Prop
🔗def
Int16.lt (a b : Int16) : Prop

{docstring UInt32.lt}

🔗def
Int32.lt (a b : Int32) : Prop
🔗def
UInt64.lt (a b : UInt64) : Prop
🔗def
Int64.lt (a b : Int64) : Prop
🔗def
USize.decEq (a b : USize) : Decidable (a = b)

Decides equality on USize. This function is overridden with a native implementation.

🔗def
ISize.decEq (a b : ISize) : Decidable (a = b)
🔗def
UInt8.decEq (a b : UInt8) : Decidable (a = b)

Decides equality on UInt8. This function is overridden with a native implementation.

🔗def
Int8.decEq (a b : Int8) : Decidable (a = b)
🔗def
UInt16.decEq (a b : UInt16) : Decidable (a = b)

Decides equality on UInt16. This function is overridden with a native implementation.

🔗def
Int16.decEq (a b : Int16) : Decidable (a = b)
🔗def
UInt32.decEq (a b : UInt32) : Decidable (a = b)

Decides equality on UInt32. This function is overridden with a native implementation.

🔗def
Int32.decEq (a b : Int32) : Decidable (a = b)
🔗def
UInt64.decEq (a b : UInt64) : Decidable (a = b)

Decides equality on UInt64. This function is overridden with a native implementation.

🔗def
Int64.decEq (a b : Int64) : Decidable (a = b)
🔗def
USize.decLe (a b : USize) : Decidable (a ≤ b)
🔗def
ISize.decLe (a b : ISize) : Decidable (a ≤ b)
🔗def
UInt8.decLe (a b : UInt8) : Decidable (a ≤ b)
🔗def
Int8.decLe (a b : Int8) : Decidable (a ≤ b)
🔗def
UInt16.decLe (a b : UInt16) : Decidable (a ≤ b)
🔗def
Int16.decLe (a b : Int16) : Decidable (a ≤ b)
🔗def
UInt32.decLe (a b : UInt32) : Decidable (a ≤ b)

Decides less-than on UInt32. This function is overridden with a native implementation.

🔗def
Int32.decLe (a b : Int32) : Decidable (a ≤ b)
🔗def
UInt64.decLe (a b : UInt64) : Decidable (a ≤ b)
🔗def
Int64.decLe (a b : Int64) : Decidable (a ≤ b)
🔗def
USize.decLt (a b : USize) : Decidable (a < b)
🔗def
ISize.decLt (a b : ISize) : Decidable (a < b)
🔗def
UInt8.decLt (a b : UInt8) : Decidable (a < b)
🔗def
Int8.decLt (a b : Int8) : Decidable (a < b)
🔗def
UInt16.decLt (a b : UInt16) : Decidable (a < b)
🔗def
Int16.decLt (a b : Int16) : Decidable (a < b)
🔗def
UInt32.decLt (a b : UInt32) : Decidable (a < b)

Decides less-equal on UInt32. This function is overridden with a native implementation.

🔗def
Int32.decLt (a b : Int32) : Decidable (a < b)
🔗def
UInt64.decLt (a b : UInt64) : Decidable (a < b)
🔗def
Int64.decLt (a b : Int64) : Decidable (a < b)

12.4.4.4. 算術（Arithmetic）🔗

通常、固定長整数に対する算術操作は Lean のオーバーロードされた算術記法を用いてアクセスするべきであり、特に Add ・ Sub ・ Mul ・ Div ・ and Mod ・符号付き型の Neg のインスタンスを使用します。

🔗def
ISize.neg (i : ISize) : ISize
🔗def
Int8.neg (i : Int8) : Int8
🔗def
Int16.neg (i : Int16) : Int16
🔗def
Int32.neg (i : Int32) : Int32
🔗def
Int64.neg (i : Int64) : Int64
🔗def
USize.add (a b : USize) : USize
🔗def
ISize.add (a b : ISize) : ISize
🔗def
UInt8.add (a b : UInt8) : UInt8
🔗def
Int8.add (a b : Int8) : Int8
🔗def
UInt16.add (a b : UInt16) : UInt16
🔗def
Int16.add (a b : Int16) : Int16
🔗def
UInt32.add (a b : UInt32) : UInt32
🔗def
Int32.add (a b : Int32) : Int32
🔗def
UInt64.add (a b : UInt64) : UInt64
🔗def
Int64.add (a b : Int64) : Int64
🔗def
USize.sub (a b : USize) : USize
🔗def
ISize.sub (a b : ISize) : ISize
🔗def
UInt8.sub (a b : UInt8) : UInt8
🔗def
Int8.sub (a b : Int8) : Int8
🔗def
UInt16.sub (a b : UInt16) : UInt16
🔗def
Int16.sub (a b : Int16) : Int16
🔗def
UInt32.sub (a b : UInt32) : UInt32
🔗def
Int32.sub (a b : Int32) : Int32
🔗def
UInt64.sub (a b : UInt64) : UInt64
🔗def
Int64.sub (a b : Int64) : Int64
🔗def
USize.mul (a b : USize) : USize
🔗def
ISize.mul (a b : ISize) : ISize
🔗def
UInt8.mul (a b : UInt8) : UInt8
🔗def
Int8.mul (a b : Int8) : Int8
🔗def
UInt16.mul (a b : UInt16) : UInt16
🔗def
Int16.mul (a b : Int16) : Int16
🔗def
UInt32.mul (a b : UInt32) : UInt32
🔗def
Int32.mul (a b : Int32) : Int32
🔗def
UInt64.mul (a b : UInt64) : UInt64
🔗def
Int64.mul (a b : Int64) : Int64
🔗def
USize.div (a b : USize) : USize
🔗def
ISize.div (a b : ISize) : ISize
🔗def
UInt8.div (a b : UInt8) : UInt8
🔗def
Int8.div (a b : Int8) : Int8
🔗def
UInt16.div (a b : UInt16) : UInt16
🔗def
Int16.div (a b : Int16) : Int16
🔗def
UInt32.div (a b : UInt32) : UInt32
🔗def
Int32.div (a b : Int32) : Int32
🔗def
UInt64.div (a b : UInt64) : UInt64
🔗def
Int64.div (a b : Int64) : Int64
🔗def
USize.mod (a b : USize) : USize
🔗def
ISize.mod (a b : ISize) : ISize
🔗def
UInt8.mod (a b : UInt8) : UInt8
🔗def
Int8.mod (a b : Int8) : Int8
🔗def
UInt16.mod (a b : UInt16) : UInt16
🔗def
Int16.mod (a b : Int16) : Int16
🔗def
UInt32.mod (a b : UInt32) : UInt32
🔗def
Int32.mod (a b : Int32) : Int32
🔗def
UInt64.mod (a b : UInt64) : UInt64
🔗def
Int64.mod (a b : Int64) : Int64
🔗def
USize.log2 (a : USize) : USize
🔗def
UInt8.log2 (a : UInt8) : UInt8
🔗def
UInt16.log2 (a : UInt16) : UInt16
🔗def
UInt32.log2 (a : UInt32) : UInt32
🔗def
UInt64.log2 (a : UInt64) : UInt64

12.4.4.5. Bitwise Operations

通常、固定長整数に対するビット演算は、Lean のオーバーロードされた演算子によってアクセスされるべきであり、特に ShiftLeft ・ ShiftRight ・ AndOp ・ OrOp ・ Xor のインスタンスを使用します。

🔗def
USize.land (a b : USize) : USize
🔗def
ISize.land (a b : ISize) : ISize
🔗def
UInt8.land (a b : UInt8) : UInt8
🔗def
Int8.land (a b : Int8) : Int8
🔗def
UInt16.land (a b : UInt16) : UInt16
🔗def
Int16.land (a b : Int16) : Int16
🔗def
UInt32.land (a b : UInt32) : UInt32
🔗def
Int32.land (a b : Int32) : Int32
🔗def
UInt64.land (a b : UInt64) : UInt64
🔗def
Int64.land (a b : Int64) : Int64
🔗def
USize.lor (a b : USize) : USize
🔗def
ISize.lor (a b : ISize) : ISize
🔗def
UInt8.lor (a b : UInt8) : UInt8
🔗def
Int8.lor (a b : Int8) : Int8
🔗def
UInt16.lor (a b : UInt16) : UInt16
🔗def
Int16.lor (a b : Int16) : Int16
🔗def
UInt32.lor (a b : UInt32) : UInt32
🔗def
Int32.lor (a b : Int32) : Int32
🔗def
UInt64.lor (a b : UInt64) : UInt64
🔗def
Int64.lor (a b : Int64) : Int64
🔗def
USize.xor (a b : USize) : USize
🔗def
ISize.xor (a b : ISize) : ISize
🔗def
UInt8.xor (a b : UInt8) : UInt8
🔗def
Int8.xor (a b : Int8) : Int8
🔗def
UInt16.xor (a b : UInt16) : UInt16
🔗def
Int16.xor (a b : Int16) : Int16
🔗def
UInt32.xor (a b : UInt32) : UInt32
🔗def
Int32.xor (a b : Int32) : Int32
🔗def
UInt64.xor (a b : UInt64) : UInt64
🔗def
Int64.xor (a b : Int64) : Int64
🔗def
USize.complement (a : USize) : USize
🔗def
ISize.complement (a : ISize) : ISize
🔗def
UInt8.complement (a : UInt8) : UInt8
🔗def
Int8.complement (a : Int8) : Int8
🔗def
UInt16.complement (a : UInt16) : UInt16
🔗def
Int16.complement (a : Int16) : Int16
🔗def
UInt32.complement (a : UInt32) : UInt32
🔗def
Int32.complement (a : Int32) : Int32
🔗def
UInt64.complement (a : UInt64) : UInt64
🔗def
Int64.complement (a : Int64) : Int64
🔗def
USize.shiftLeft (a b : USize) : USize
🔗def
ISize.shiftLeft (a b : ISize) : ISize
🔗def
UInt8.shiftLeft (a b : UInt8) : UInt8
🔗def
Int8.shiftLeft (a b : Int8) : Int8
🔗def
UInt16.shiftLeft (a b : UInt16) : UInt16
🔗def
Int16.shiftLeft (a b : Int16) : Int16
🔗def
UInt32.shiftLeft (a b : UInt32) : UInt32
🔗def
Int32.shiftLeft (a b : Int32) : Int32
🔗def
UInt64.shiftLeft (a b : UInt64) : UInt64
🔗def
Int64.shiftLeft (a b : Int64) : Int64
🔗def
USize.shiftRight (a b : USize) : USize
🔗def
ISize.shiftRight (a b : ISize) : ISize
🔗def
UInt8.shiftRight (a b : UInt8) : UInt8
🔗def
Int8.shiftRight (a b : Int8) : Int8
🔗def
UInt16.shiftRight (a b : UInt16) : UInt16
🔗def
Int16.shiftRight (a b : Int16) : Int16
🔗def
UInt32.shiftRight (a b : UInt32) : UInt32
🔗def
Int32.shiftRight (a b : Int32) : Int32
🔗def
UInt64.shiftRight (a b : UInt64) : UInt64
🔗def
Int64.shiftRight (a b : Int64) : Int64

12.4.4.6. 証明の自動化（Proof Automation）

本節の関数は主に simp で採用される単純化規則の実装の一部です。これらはおそらく、固定長整数を含むカスタムの証明自動化を実装しているユーザにとっては興味深いものになるでしょう。

🔗def
USize.fromExpr (e : Lean.Expr)
    : Lean.Meta.SimpM (Option USize)
🔗def
UInt8.fromExpr
    : Lean.Expr → Lean.Meta.SimpM (Option UInt8)
🔗def
UInt16.fromExpr
    : Lean.Expr →
      Lean.Meta.SimpM (Option UInt16)
🔗def
UInt32.fromExpr
    : Lean.Expr →
      Lean.Meta.SimpM (Option UInt32)
🔗def
UInt64.fromExpr
    : Lean.Expr →
      Lean.Meta.SimpM (Option UInt64)
🔗def
UInt8.reduceAdd : Lean.Meta.Simp.DSimproc
🔗def
UInt16.reduceAdd : Lean.Meta.Simp.DSimproc
🔗def
UInt32.reduceAdd : Lean.Meta.Simp.DSimproc
🔗def
UInt64.reduceAdd : Lean.Meta.Simp.DSimproc
🔗def
UInt8.reduceDiv : Lean.Meta.Simp.DSimproc
🔗def
UInt16.reduceDiv : Lean.Meta.Simp.DSimproc
🔗def
UInt32.reduceDiv : Lean.Meta.Simp.DSimproc
🔗def
UInt64.reduceDiv : Lean.Meta.Simp.DSimproc
🔗def
UInt8.reduceGE : Lean.Meta.Simp.Simproc
🔗def
UInt16.reduceGE : Lean.Meta.Simp.Simproc
🔗def
UInt32.reduceGE : Lean.Meta.Simp.Simproc
🔗def
UInt64.reduceGE : Lean.Meta.Simp.Simproc
🔗def
UInt8.reduceGT : Lean.Meta.Simp.Simproc
🔗def
UInt16.reduceGT : Lean.Meta.Simp.Simproc
🔗def
UInt32.reduceGT : Lean.Meta.Simp.Simproc
🔗def
UInt64.reduceGT : Lean.Meta.Simp.Simproc
🔗def
UInt8.reduceLE : Lean.Meta.Simp.Simproc
🔗def
UInt16.reduceLE : Lean.Meta.Simp.Simproc
🔗def
UInt32.reduceLE : Lean.Meta.Simp.Simproc
🔗def
UInt64.reduceLE : Lean.Meta.Simp.Simproc
🔗def
UInt8.reduceLT : Lean.Meta.Simp.Simproc
🔗def
UInt16.reduceLT : Lean.Meta.Simp.Simproc
🔗def
UInt32.reduceLT : Lean.Meta.Simp.Simproc
🔗def
UInt64.reduceLT : Lean.Meta.Simp.Simproc
🔗def
UInt8.reduceMod : Lean.Meta.Simp.DSimproc
🔗def
UInt16.reduceMod : Lean.Meta.Simp.DSimproc
🔗def
UInt32.reduceMod : Lean.Meta.Simp.DSimproc
🔗def
UInt64.reduceMod : Lean.Meta.Simp.DSimproc
🔗def
UInt8.reduceMul : Lean.Meta.Simp.DSimproc
🔗def
UInt16.reduceMul : Lean.Meta.Simp.DSimproc
🔗def
UInt32.reduceMul : Lean.Meta.Simp.DSimproc
🔗def
UInt64.reduceMul : Lean.Meta.Simp.DSimproc
🔗def
UInt8.reduceOfNat : Lean.Meta.Simp.DSimproc
🔗def
UInt16.reduceOfNat : Lean.Meta.Simp.DSimproc
🔗def
UInt32.reduceOfNat : Lean.Meta.Simp.DSimproc
🔗def
UInt64.reduceOfNat : Lean.Meta.Simp.DSimproc
🔗def
UInt8.reduceOfNatCore : Lean.Meta.Simp.DSimproc
🔗def
UInt16.reduceOfNatCore : Lean.Meta.Simp.DSimproc
🔗def
UInt32.reduceOfNatCore : Lean.Meta.Simp.DSimproc
🔗def
UInt64.reduceOfNatCore : Lean.Meta.Simp.DSimproc
🔗def
UInt8.reduceSub : Lean.Meta.Simp.DSimproc
🔗def
UInt16.reduceSub : Lean.Meta.Simp.DSimproc
🔗def
UInt32.reduceSub : Lean.Meta.Simp.DSimproc
🔗def
UInt64.reduceSub : Lean.Meta.Simp.DSimproc
🔗def
USize.reduceToNat : Lean.Meta.Simp.Simproc
🔗def
UInt8.reduceToNat : Lean.Meta.Simp.DSimproc
🔗def
UInt16.reduceToNat : Lean.Meta.Simp.DSimproc
🔗def
UInt32.reduceToNat : Lean.Meta.Simp.DSimproc
🔗def
UInt64.reduceToNat : Lean.Meta.Simp.DSimproc