←Prev ↑Up Next→

The Lean Language Reference 日本語訳

1.	はじめに（Introduction）
2.	エラボレーションとコンパイル（Elaboration and Compilation）
3.	型システム（The Type System）
4.	ソースファイル（Source Files）
5.	再帰定義（Recursive Definitions）
6.	項（Terms）
7.	型クラス（Type Classes）
8.	関手・モナド・do記法（Functors, Monads and `do`-Notation）
9.	IO
10.	タクティクによる証明（Tactic Proofs）
11.	単純化器（The Simplifier）
12.	基本的な型（Basic Types）
13.	Standard Library
14.	記法とマクロ（Notations and Macros）
15.	Output from Lean
16.	Elan
17.	Lake and Reservoir
	Index
18.	この翻訳について

12. 基本的な型（Basic Types）

12.1.	自然数（Natural Numbers）
12.2.	整数
12.3.	有限な自然数
12.4.	固定精度整数型（Fixed-Precision Integer Types）
12.5.	Bitvectors
12.6.	Floating-Point Numbers
12.7.	文字（Characters）
12.8.	文字列（Strings）
12.9.	ユニット型（The Unit Type）
12.10.	空の型（The Empty Type）
12.11.	真偽値（Booleans）
12.12.	オプショナルの値
12.13.	Tuples
12.14.	Sum Types
12.15.	Dependent Pairs
12.16.	Linked Lists
12.17.	配列（Arrays）
12.18.	Subtypes
12.19.	Lazy Computations
12.20.	Tasks and Threads

12.5. Bitvectors

Source Code
Report Issues

12.5. Bitvectors🔗

Planned Content

Run-time and kernel representations of BitVec
API reference
Cross-reference to TBW chapter on bv_decide

Tracked at issue #106