Skip to content

Commit 665d016

Browse files
committed
chore: finish cleanup
1 parent 4d7e0bb commit 665d016

2 files changed

Lines changed: 1 addition & 2 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

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)