Merge pull request #904 from lean-ja/Seasawher/issue888

Char 型を紹介する

.lycheeignore

@@ -1,5 +1,6 @@
 https://raw.githubusercontent.com/lean-ja/lean-by-example/.*
 https://adam.math.hhu.de/#/g/leanprover-community/NNG4
+https://lean-lang.org/*
 https://live.lean-lang.org/
 https://reservoir.lean-lang.org/
 https://dcbadge.limes.pink/api/server/*

Examples/Type/Char.lean

@@ -0,0 +1,42 @@
+/- # Char
+`Char` 型は、Unicode 文字を表します。二重引用符 `"` ではなくてシングルクォート `'` で囲んで表されます。
+-/
+
+-- Char はシングルクォートで囲む
+#check ('a' : Char)
+#check ("a" : String)
+
+-- Unicode 文字を含む
+#check ('あ' : Char)
+#check ('∀' : Char)
+#check ('∅' : Char)
+
+/- `Char` は、以下のように [`structure`](../Declarative/Structure.md) として定義されています。 -/
+
+--#--
+-- Char の定義が変わっていないことを確認するためのコード
+/--
+info: structure Char : Type
+number of parameters: 0
+constructor:
+Char.mk : (val : UInt32) → val.isValidChar → Char
+fields:
+val : UInt32
+valid : self.val.isValidChar
+-/
+#guard_msgs in #print Char
+--#--
+namespace Hidden --#
+
+structure Char where
+  /-- Unicode スカラー値 -/
+  val : UInt32
+
+  /-- `val` が正しいコードポイントであること -/
+  valid : val.isValidChar
+
+end Hidden --#
+/- したがって `Char.val` 関数によりコードポイントを取得することができます。-/
+
+#guard 'a'.val = 97
+#guard '⨅'.val = 10757

Examples/Type/String.lean

@@ -1,6 +1,6 @@
 /- # String
 
-`String` は文字列を表す型です。次のように、文字を表す型 `Char` のリストとして定義されています。
+`String` は文字列を表す型です。次のように、文字を表す型 [`Char`](./Char.md) のリストとして定義されています。
 -/
 import Lean --#
 --#--
@@ -24,18 +24,15 @@ structure String where
   data : List Char
 
 end Hidden --#
-/- ## 基本的な操作
 
-文字列に関する基本的な操作を紹介します。-/
-
-/- ### 文字列結合
+/- ## 文字列結合
 `String.append` を使って文字列を結合することができます。この関数は `++` という記号が割り当てられています。
 -/
 
 #guard String.append "Hello, " "world!" = "Hello, world!"
 #guard "Hello, " ++ "world!" = "Hello, world!"
 
-/- ### 文字列の長さ
+/- ## 文字列の長さ
 文字列の長さは `String.length` 関数で取得することができます。
 -/
 
@@ -69,7 +66,7 @@ and both `String.utf8ByteSize` and `String.length` are cached and O(1).
 -/
 #guard_msgs in #doc String
 
-/- ### 文字列補完
+/- ## 文字列補完
 
 `String` 型の変数の「評価した後の値」を文字列に埋め込むことができます。これを文字列補完と呼びます。Lean では、これは `s!` という構文で行うことができます。
 -/

src/SUMMARY.md

@@ -83,6 +83,7 @@
   - [ToString: 文字列に変換](./TypeClass/ToString.md)
 
 - [型](./Type/README.md)
+  - [Char: Unicode 文字](./Type/Char.md)
   - [Prop: 命題全体](./Type/Prop.md)
   - [String: 文字列](./Type/String.md)
   - [Type: 型全体](./Type/Type.md)