Skip to content

Commit 8b24774

Browse files
committed
chore: finish cleanup
1 parent 4d7e0bb commit 8b24774

3 files changed

Lines changed: 1 addition & 3 deletions

File tree

UnicodeBasic.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -732,5 +732,3 @@ public def isAlphabetic (char : Char) : Bool :=
732732

733733
@[inherit_doc isAlphabetic]
734734
public abbrev isAlpha := isAlphabetic
735-
736-
end Unicode

lakefile.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ import Lake
77
open System Lake DSL
88

99
package UnicodeBasic where
10-
version := v!"1.1.0"
1110
description := "Basic Unicode support for Lean 4"
1211
keywords := #["unicode"]
1312
reservoir := true

makeCLib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
module
12
import UnicodeData
23

34
open Unicode

0 commit comments

Comments
 (0)