You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: README.md
+29-12Lines changed: 29 additions & 12 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -1,28 +1,45 @@
1
1
# Lean 4 / Unicode Basic
2
2
3
-
Lightweight Unicode support for Lean 4.
3
+
Unicode support for Lean 4.
4
4
5
-
Unicode properties that are currently supported are:
5
+
Unicode properties that are currently supported by `UnicodeBasic` include:
6
6
7
7
*`Alphabetic`
8
-
*`Bidi_Class`, `Bidi_Control`, and `Bidi_Mirrored`
8
+
*`Bidi_Class`
9
+
*`Bidi_Control`
10
+
*`Bidi_Mirrored`
9
11
*`Canonical_Combining_Class`
10
-
*`Uppercase`, `Lowercase`, `Cased` and `Case_Ignorable`
11
-
*`Decomposition_Type` and `Decomposition_Mapping`
12
+
*`Case_Ignorable`
13
+
*`Cased`
14
+
*`Decomposition_Mapping`
15
+
*`Decomposition_Type`
12
16
*`General_Category`
13
17
*`Hex_Digit`
14
18
*`Math`
15
19
*`Name`
16
-
*`Numeric_Type` and `Numeric_Value`
17
-
*`Simple_Lowercase_Mapping`, `Simple_Uppercase_Mapping`, and `Simple_Titlecase_Mapping`
20
+
*`Numeric_Type`
21
+
*`Numeric_Value`
22
+
*`Simple_Lowercase_Mapping`
23
+
*`Simple_Uppercase_Mapping`
24
+
*`Simple_Titlecase_Mapping`
25
+
*`Lowercase`
26
+
*`Uppercase`
18
27
*`White_Space`
19
28
20
-
To keep the library lightweight, only properties that can be derived exclusively from `UnicodeData.txt` and `PropList.txt` can be supported.
21
-
If you need a property not yet in the list above, please submit a feature request!
29
+
To keep the `UnicodeLibrary` library lightweight, only commonly used properties can be supported. If you need a property not yet in the list above, please submit a feature request!
22
30
23
31
## Installation
24
32
25
-
Add the following dependency to your project's `lakefile.lean`:
33
+
Add the following dependency to your project's `lakefile.toml`:
0 commit comments