doc: builtin types

doc/SUMMARY.md

@@ -17,10 +17,21 @@
   - [Implicit Arguments](./implicit.md)
   - [Auto Bound Implicit Arguments](./autobound.md)
 - [Functions](./functions.md)
+- [Builtin Types](./builtintypes.md)
+  - [Natural number](./nat.md)
+  - [Integer](./int.md)
+  - [Fixed precision unsigned integer](./uint.md)
+  - [Float](./float.md)
+  - [Array](./array.md)
+  - [List](./list.md)
+  - [Character](./char.md)
+  - [String](./string.md)
+  - [Option](./option.md)
+  - [Thunk](./thunk.md)
+  - [Task and Thread](./task.md)
 - [Type classes](./typeclass.md)
 - [The `do` Notation](./do.md)
 - [Tactics](./tactics.md)
-- [Thunks, Tasks and Threads](./thunks.md)
 - [String interpolation](./stringinterp.md)
 
 # Other

doc/array.md

@@ -0,0 +1 @@
+# Array

doc/builtintypes.md

@@ -0,0 +1,25 @@
+# Builtin Types
+
+## Numeric Operations
+
+Lean supports the basic mathematical operations you’d expect for all of the number types: addition, subtraction, multiplication, division, and remainder.
+The following code shows how you’d use each one in a `def` commands:
+
+```lean
+-- addition
+def sum := 5 + 10
+
+-- subtraction
+def difference := 95.5 - 4.3
+
+-- multiplication
+def product := 4 * 30
+
+-- division
+def quotient := 53.7 / 32.2
+
+-- remainder/modulo
+def modulo := 43 % 5
+```
+
+Each expression in these statements uses a mathematical operator and evaluates to a single value.

doc/char.md

@@ -0,0 +1 @@
+# Characters

doc/float.md

@@ -0,0 +1 @@
+# Float

doc/int.md

@@ -0,0 +1,37 @@
+# Integers
+
+The `Int` type represents the arbitrary-precision integers. There are no overflows.
+```lean
+#eval (100000000000000000 : Int) * 200000000000000000000 * 1000000000000000000000
+```
+Recall that nonnegative numerals are considered to be a `Nat` if there are no typing constraints.
+```lean
+#check 1 -- Nat
+#check -1 -- Int
+#check (1:Int) -- Int
+```
+
+The operator `/` for `Int` implements integer division.
+```lean
+#eval -10 / 4 -- -2
+```
+
+Similar to the `Nat, the internal representation of `Int` is optimized. Small integers are
+represented by a single machine word. Big integers are implemented using [GMP](https://gmplib.org/manual/) numbers.
+We recommend you use fixed precision numeric types only in performance critical code.
+
+The Lean kernel has not special support for reducing `Int` during type checking.
+However, since `Int` is defined as
+```lean
+# namespace hidden
+inductive Int : Type where
+  | ofNat   : Nat → Int
+  | negSucc : Nat → Int
+# end hidden
+```
+the type checker will be able reduce `Int` expressions efficiently by relying on the special support for `Nat`.
+
+```lean
+theorem ex : -2000000000 * 1000000000 = -2000000000000000000 :=
+ rfl
+```

doc/list.md

@@ -0,0 +1 @@
+# List

doc/nat.md

@@ -0,0 +1,68 @@
+# Natural numbers
+
+The `Nat` type represents the natural numbers, i.e., arbitrary-precision unsigned integers.
+There are no overflows.
+
+```lean
+#eval 100000000000000000 * 200000000000000000000 * 1000000000000000000000
+```
+
+A numeral is considered to be a `Nat` if there are no typing constraints.
+```lean
+#check 10    -- Nat
+#check id 10 -- Nat
+
+def f (x : Int) : Int :=
+  x - 1
+
+#eval f (3 - 5) -- 3 and 5 are `Int` since `f` expects an `Int`.
+-- -3
+```
+
+The operator `-` for `Nat` implements truncated subtraction.
+```lean
+#eval 10 - 5 -- 5
+#eval 5 - 10 -- 0
+
+theorem ex : 5 - 10 = 0 :=
+  rfl
+
+#eval (5:Int) - 10 -- -5
+```
+
+The operator `/` for `Nat` implements Euclidean division.
+```lean
+#eval 10 / 4 -- 2
+
+#check 10.0 / 4.0 -- Float
+#eval 10.0 / 4.0  -- 2.5
+```
+
+As we described in the previous sections, we define the `Nat` type as an `inductive` datatype.
+```lean
+# namespace hidden
+inductive Nat where
+ | zero : Nat
+ | succ : Nat → Nat
+# end hidden
+```
+However, the internal representation of `Nat` is optimized. Small natural numbers (i.e., < `2^63` in a 64-bit machine) are
+represented by a single machine word. Big numbers are implemented using [GMP](https://gmplib.org/manual/) numbers.
+We recommend you use fixed precision numeric types only in performance critical code.
+
+The Lean kernel has builtin support for the `Nat` type too, and can efficiently reduce `Nat` expressions during type checking.
+```lean
+#reduce 100000000000000000 * 200000000000000000000 * 1000000000000000000000
+
+theorem ex
+      : 1000000000000000 * 2000000000000000000 = 2000000000000000000000000000000000 :=
+  rfl
+```
+The sharp-eyed reader will notice that GMP is part of the Lean kernel trusted code base.
+We believe this is not a problem because you can use external type checkers to double-check your developments,
+and we consider GMP very thrustworthy.
+Existing external type checkers for Lean 3 (e.g., [Trepplein](https://github.com/gebner/trepplein) and [TC](https://github.com/leanprover/tc))
+can be easily adapted to Lean 4.
+If you are still concerned after checking your development with multiple different external checkers because
+they may all rely on buggy arbitrary-precision libraries,
+you can develop your own certified arbitrary-precision library and use it to implement your own type checker for Lean.

doc/option.md

@@ -0,0 +1 @@
+# Option

doc/string.md

@@ -0,0 +1 @@
+# Strings

doc/task.md

@@ -0,0 +1 @@
+# Task

doc/thunk.md

@@ -102,11 +102,3 @@ and `add1` is still considered to be a pure function.
 The Lean compiler performs common subexpression elimination when compiling `double`,
 and the produced code for `double` executes `x ()` only once instead of twice.
 This transformation is safe because `x : Unit -> Nat` is pure.
-
-## Tasks
-
-TODO
-
-## Threads
-
-TODO

doc/uint.md

@@ -0,0 +1 @@
+# Fixed precision unsigned integers