Skip to content

Commit 6b0500d

Browse files
committed
fix: public data
1 parent 07e15ce commit 6b0500d

3 files changed

Lines changed: 3 additions & 3 deletions

File tree

UnicodeData/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,7 @@ def UnicodeData.mkTangutIdeograph (c : UInt32) : UnicodeData where
115115
protected def UnicodeData.txt := include_str "../data/UnicodeData.txt"
116116

117117
/-- Parse `UnicodeData.txt` -/
118-
unsafe initialize UnicodeData.data : Array UnicodeData ←
118+
public unsafe initialize UnicodeData.data : Array UnicodeData ←
119119
let getDecompositionMapping? (s : String.Slice) : Option DecompositionMapping := do
120120
/-
121121
The value of the `Decomposition_Mapping` property for a character is

UnicodeData/PropList.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ deriving Inhabited, Repr
3535
/-- Raw string form `PropList.txt` -/
3636
protected def PropList.txt := include_str "../data/PropList.txt"
3737

38-
unsafe initialize PropList.data : PropList ←
38+
public unsafe initialize PropList.data : PropList ←
3939
let stream := UCDStream.ofString PropList.txt
4040
let mut list : PropList := {}
4141
for record in stream do

UnicodeData/Scripts.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ public abbrev Scripts := Std.HashMap String.Slice (Array (UInt32 × UInt32))
1515
/-- Raw string from `Scripts.txt` -/
1616
def Scripts.txt := include_str "../data/Scripts.txt"
1717

18-
initialize Scripts.data : Scripts ← do
18+
public initialize Scripts.data : Scripts ← do
1919
let stream := UCDStream.ofString Scripts.txt
2020
let mut t := {}
2121
for record in stream do

0 commit comments

Comments
 (0)