From a9f23f8ca34914dc4bd5f314ac52ccf669def0fb Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 24 Nov 2025 17:59:53 -0500 Subject: [PATCH] chore: remove deprecations --- UnicodeBasic.lean | 141 -------------------- UnicodeBasic/TableLookup.lean | 5 - UnicodeBasic/Types.lean | 243 ---------------------------------- UnicodeData/Basic.lean | 28 ---- 4 files changed, 417 deletions(-) diff --git a/UnicodeBasic.lean b/UnicodeBasic.lean index e587cefb4..e2d959cc8 100644 --- a/UnicodeBasic.lean +++ b/UnicodeBasic.lean @@ -114,32 +114,11 @@ where .Sk, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ll, .Ps, .Sm, .Po, .Sm, .Cc] -set_option linter.deprecated false in -@[deprecated Unicode.getGC (since := "1.2.0")] -def getGeneralCategory (char : Char) : GeneralCategory := - .ofGC! (getGC char) - instance : Membership Char GC where mem cat char := getGC char ⊆ cat instance (char : Char) (cat : GC) : Decidable (char ∈ cat) := inferInstanceAs (Decidable (_ ⊆ _)) -set_option linter.deprecated false in -@[deprecated "use `char ∈ category` instead" (since := "1.2.0")] -def isInGeneralCategory (char : Char) (category : GeneralCategory) : Bool := - match category, getGeneralCategory char with - | ⟨major, none⟩, ⟨charMajor, _⟩ => major == charMajor - | ⟨_, some .casedLetter⟩, ⟨_, some .lowercaseLetter⟩ => true - | ⟨_, some .casedLetter⟩, ⟨_, some .titlecaseLetter⟩ => true - | ⟨_, some .casedLetter⟩, ⟨_, some .uppercaseLetter⟩ => true - | ⟨_, some .casedLetter⟩, _ => false - | ⟨_, some .groupPunctuation⟩, ⟨_, some .openPunctuation⟩ => true - | ⟨_, some .groupPunctuation⟩, ⟨_, some .closePunctuation⟩ => true - | ⟨_, some .groupPunctuation⟩, _ => false - | ⟨_, some .quotePunctuation⟩, ⟨_, some .initialPunctuation⟩ => true - | ⟨_, some .quotePunctuation⟩, ⟨_, some .finalPunctuation⟩ => true - | ⟨_, some .quotePunctuation⟩, _ => false - | cat, charCat => cat == charCat namespace GeneralCategory @@ -150,33 +129,21 @@ namespace GeneralCategory Unicode Property: `General_Category=L` -/ abbrev isLetter (char : Char) : Bool := char ∈ Unicode.GC.L -@[deprecated "c ∈ Unicode.GC.L" (since := "1.2.0")] -protected abbrev isL := isLetter - /-- Check if lowercase letter character (`Ll`) Unicode Property: `General_Category=Ll` -/ abbrev isLowercaseLetter (char : Char) : Bool := char ∈ Unicode.GC.Ll -@[deprecated "c ∈ Unicode.GC.Ll" (since := "1.2.0")] -protected abbrev isLl := isLowercaseLetter - /-- Check if titlecase letter character (`Lt`) Unicode Property: `General_Category=Lt` -/ abbrev isTitlecaseLetter (char : Char) : Bool := char ∈ Unicode.GC.Lt -@[deprecated "c ∈ Unicode.GC.Lt" (since := "1.2.0")] -protected abbrev isLt := isTitlecaseLetter - /-- Check if uppercase letter character (`Lu`) Unicode Property: `General_Category=Lu` -/ abbrev isUppercaseLetter (char : Char) : Bool := char ∈ Unicode.GC.Lu -@[deprecated "c ∈ Unicode.GC.Lu" (since := "1.2.0")] -protected abbrev isLu := isUppercaseLetter - /-- Check if cased letter character (`LC`) This is a derived category (`L = Lu | Ll | Lt`). @@ -184,25 +151,16 @@ protected abbrev isLu := isUppercaseLetter Unicode Property: `General_Category=LC` -/ abbrev isCasedLetter (char : Char) : Bool := char ∈ Unicode.GC.LC -@[deprecated "c ∈ Unicode.GC.LC" (since := "1.2.0")] -protected abbrev isLC := isCasedLetter - /-- Check if modifier letter character (`Lm`) Unicode Property: `General_Category=Lm`-/ abbrev isModifierLetter (char : Char) : Bool := char ∈ Unicode.GC.Lm -@[deprecated "c ∈ Unicode.GC.Lm" (since := "1.2.0")] -protected abbrev isLm := isModifierLetter - /-- Check if other letter character (`Lo`) Unicode Property: `General_Category=Lo`-/ abbrev isOtherLetter (char : Char) : Bool := char ∈ Unicode.GC.Lo -@[deprecated "c ∈ Unicode.GC.Lo" (since := "1.2.0")] -protected abbrev isLo := isOtherLetter - /-- Check if mark character (`M`) This is a derived category (`M = Mn | Mc | Me`). @@ -210,33 +168,21 @@ protected abbrev isLo := isOtherLetter Unicode Property: `General_Category=M` -/ abbrev isMark (char : Char) : Bool := char ∈ Unicode.GC.M -@[deprecated "c ∈ Unicode.GC.M" (since := "1.2.0")] -protected abbrev isM := isMark - /-- Check if nonspacing combining mark character (`Mn`) Unicode Property: `General_Category=Mn` -/ abbrev isNonspacingMark (char : Char) : Bool := char ∈ Unicode.GC.Mn -@[deprecated "c ∈ Unicode.GC.Mn" (since := "1.2.0")] -protected abbrev isMn := isNonspacingMark - /-- Check if spacing combining mark character (`Mc`) Unicode Property: `General_Category=Mc` -/ abbrev isSpacingMark (char : Char) : Bool := char ∈ Unicode.GC.Mc -@[deprecated "c ∈ Unicode.GC.Mc" (since := "1.2.0")] -protected abbrev isMc := isSpacingMark - /-- Check if enclosing combining mark character (`Me`) Unicode Property: `General_Category=Me` -/ abbrev isEnclosingMark (char : Char) : Bool := char ∈ Unicode.GC.Me -@[deprecated "c ∈ Unicode.GC.Me" (since := "1.2.0")] -protected abbrev isMe := isEnclosingMark - /-- Check if number character (`N`) This is a derived category (`N = Nd | Nl | No`). @@ -244,33 +190,21 @@ protected abbrev isMe := isEnclosingMark Unicode Property: `General_Category=N` -/ abbrev isNumber (char : Char) : Bool := char ∈ Unicode.GC.N -@[deprecated "c ∈ Unicode.GC.N" (since := "1.2.0")] -protected abbrev isN := isNumber - /-- Check if decimal number character (`Nd`) Unicode Property: `General_Category=Nd` -/ abbrev isDecimalNumber (char : Char) : Bool := char ∈ Unicode.GC.Nd -@[deprecated "c ∈ Unicode.GC.Nd" (since := "1.2.0")] -protected abbrev isNd := isDecimalNumber - /-- Check if letter number character (`Nl`) Unicode Property: `General_Category=Nl` -/ abbrev isLetterNumber (char : Char) : Bool := char ∈ Unicode.GC.Nl -@[deprecated "c ∈ Unicode.GC.Nl" (since := "1.2.0")] -protected abbrev isNl := isLetterNumber - /-- Check if other number character (`No`) Unicode Property: `General_Category=No` -/ abbrev isOtherNumber (char : Char) : Bool := char ∈ Unicode.GC.No -@[deprecated "c ∈ Unicode.GC.No" (since := "1.2.0")] -protected abbrev isNo := isOtherNumber - /-- Check if punctuation character (`P`) This is a derived category (`P = Pc | Pd | Ps | Pe | Pi | Pf | Po`). @@ -278,25 +212,16 @@ protected abbrev isNo := isOtherNumber Unicode Property: `General_Category=P` -/ abbrev isPunctuation (char : Char) : Bool := char ∈ Unicode.GC.P -@[deprecated "c ∈ Unicode.GC.P" (since := "1.2.0")] -protected abbrev isP := isPunctuation - /-- Check if connector punctuation character (`Pc`) Unicode Property: `General_Category=Pc` -/ abbrev isConnectorPunctuation (char : Char) : Bool := char ∈ Unicode.GC.Pc -@[deprecated "c ∈ Unicode.GC.Pc" (since := "1.2.0")] -protected abbrev isPc := isConnectorPunctuation - /-- Check if dash punctuation character (`Pd`) Unicode Property: `General_Category=Pd` -/ abbrev isDashPunctuation (char : Char) : Bool := char ∈ Unicode.GC.Pd -@[deprecated "c ∈ Unicode.GC.Pd" (since := "1.2.0")] -protected abbrev isPd := isDashPunctuation - /-- Check if grouping punctuation character (`PG`) This is a derived category (`PG = Ps | Pe`). @@ -304,25 +229,16 @@ protected abbrev isPd := isDashPunctuation Unicode Property: `General_Category=PG` -/ abbrev isGroupPunctuation (char : Char) : Bool := char ∈ Unicode.GC.PG -@[deprecated "c ∈ Unicode.GC.PG" (since := "1.2.0")] -protected abbrev isPG := isGroupPunctuation - /-- Check if open punctuation character (`Ps`) Unicode Property: `General_Category=Ps` -/ abbrev isOpenPunctuation (char : Char) : Bool := char ∈ Unicode.GC.Ps -@[deprecated "c ∈ Unicode.GC.Ps" (since := "1.2.0")] -protected abbrev isPs := isOpenPunctuation - /-- Check if close punctuation character (`Pe`) Unicode Property: `General_Category=Pe` -/ abbrev isClosePunctuation (char : Char) : Bool := char ∈ Unicode.GC.Pe -@[deprecated "c ∈ Unicode.GC.Pe" (since := "1.2.0")] -protected abbrev isPe := isClosePunctuation - /-- Check if quoting punctuation character (`PQ`) This is a derived category (`PQ = Pi | Pf`). @@ -330,33 +246,21 @@ protected abbrev isPe := isClosePunctuation Unicode Property: `General_Category=PQ` -/ abbrev isQuotePunctuation (char : Char) : Bool := char ∈ Unicode.GC.PQ -@[deprecated "c ∈ Unicode.GC.PQ" (since := "1.2.0")] -protected abbrev isPQ := isQuotePunctuation - /-- Check if initial punctuation character (`Pi`) Unicode Property: `General_Category=Pi` -/ abbrev isInitialPunctuation (char : Char) : Bool := char ∈ Unicode.GC.Pi -@[deprecated "c ∈ Unicode.GC.Pi" (since := "1.2.0")] -protected abbrev isPi := isInitialPunctuation - /-- Check if initial punctuation character (`Pf`) Unicode Property: `General_Category=Pf` -/ abbrev isFinalPunctuation (char : Char) : Bool := char ∈ Unicode.GC.Pf -@[deprecated "c ∈ Unicode.GC.Pf" (since := "1.2.0")] -protected abbrev isPf := isFinalPunctuation - /-- Check if other punctuation character (`Po`) Unicode Property: `General_Category=Po` -/ abbrev isOtherPunctuation (char : Char) : Bool := char ∈ Unicode.GC.Po -@[deprecated "c ∈ Unicode.GC.Po" (since := "1.2.0")] -protected abbrev isPo := isOtherPunctuation - /-- Check if symbol character (`S`) This is a derived category (`S = Sm | Sc | Sk | So`). @@ -364,41 +268,26 @@ protected abbrev isPo := isOtherPunctuation Unicode Property: `General_Category=S` -/ abbrev isSymbol (char : Char) : Bool := char ∈ Unicode.GC.S -@[deprecated "c ∈ Unicode.GC.S" (since := "1.2.0")] -protected abbrev isS := isSymbol - /-- Check if math symbol character (`Sm`) Unicode Property: `General_Category=Sm` -/ abbrev isMathSymbol (char : Char) : Bool := char ∈ Unicode.GC.Sm -@[deprecated "c ∈ Unicode.GC.Sm" (since := "1.2.0")] -protected abbrev isSm := isMathSymbol - /-- Check if currency symbol character (`Sc`) Unicode Property: `General_Category=Sc` -/ abbrev isCurrencySymbol (char : Char) : Bool := char ∈ Unicode.GC.Sc -@[deprecated "c ∈ Unicode.GC.Sc" (since := "1.2.0")] -protected abbrev isSc := isCurrencySymbol - /-- Check if modifier symbol character (`Sk`) Unicode Property: `General_Category=Sk` -/ abbrev isModifierSymbol (char : Char) : Bool := char ∈ Unicode.GC.Sk -@[deprecated "c ∈ Unicode.GC.Sk" (since := "1.2.0")] -protected abbrev isSk := isModifierSymbol - /-- Check if other symbol character (`So`) Unicode Property: `General_Category=So` -/ abbrev isOtherSymbol (char : Char) : Bool := char ∈ Unicode.GC.So -@[deprecated "c ∈ Unicode.GC.So" (since := "1.2.0")] -protected abbrev isSo := isOtherSymbol - /-- Check if separator character (`Z`) This is a derived property (`Z = Zs | Zl | Zp`). @@ -406,33 +295,21 @@ protected abbrev isSo := isOtherSymbol Unicode Property: `General_Category=Z` -/ abbrev isSeparator (char : Char) : Bool := char ∈ Unicode.GC.Z -@[deprecated "c ∈ Unicode.GC.Z" (since := "1.2.0")] -protected abbrev isZ := isSeparator - /-- Check if space separator character (`Zs`) Unicode Property: `General_Category=Zs` -/ abbrev isSpaceSeparator (char : Char) : Bool := char ∈ Unicode.GC.Zs -@[deprecated "c ∈ Unicode.GC.Zs" (since := "1.2.0")] -protected abbrev isZs := isSpaceSeparator - /-- Check if line separator character (`Zl`) Unicode Property: `General_Category=Zl` -/ abbrev isLineSeparator (char : Char) : Bool := char ∈ Unicode.GC.Zl -@[deprecated "c ∈ Unicode.GC.Zl" (since := "1.2.0")] -protected abbrev isZl := isLineSeparator - /-- Check if paragraph separator character (`Zp`) Unicode Property: `General_Category=Zp` -/ abbrev isParagraphSeparator (char : Char) : Bool := char ∈ Unicode.GC.Zp -@[deprecated "c ∈ Unicode.GC.Zp" (since := "1.2.0")] -protected abbrev isZp := isParagraphSeparator - /-- Check if other character (`C`) This is a derived category (`C = Cc | Cf | Cs | Co | Cn`). @@ -440,25 +317,16 @@ protected abbrev isZp := isParagraphSeparator Unicode Property: `General_Category=C` -/ abbrev isOther (char : Char) : Bool := char ∈ Unicode.GC.C -@[deprecated "c ∈ Unicode.GC.C" (since := "1.2.0")] -protected abbrev isC := isOther - /-- Check if control character (`Cc`) Unicode Property: `General_Category=Cc` -/ abbrev isControl (char : Char) : Bool := char ∈ Unicode.GC.Cc -@[deprecated "c ∈ Unicode.GC.Cc" (since := "1.2.0")] -protected abbrev isCc := isControl - /-- Check if format character (`Cf`) Unicode Property: `General_Category=Cf` -/ abbrev isFormat (char : Char) : Bool := char ∈ Unicode.GC.Cf -@[deprecated "c ∈ Unicode.GC.Cf" (since := "1.2.0")] -protected abbrev isCf := isFormat - /-- Check if surrogate character (`Cs`) Does not actually occur since Lean does not regard surrogate code points as characters. @@ -466,25 +334,16 @@ protected abbrev isCf := isFormat Unicode Property: `General_Category=Cs` -/ abbrev isSurrogate (char : Char) : Bool := char ∈ Unicode.GC.Cs -@[deprecated "c ∈ Unicode.GC.Cs" (since := "1.2.0")] -protected abbrev isCs := isSurrogate - /-- Check if private use character (`Co`) Unicode Property: `General_Category=Co` -/ abbrev isPrivateUse (char : Char) : Bool := char ∈ Unicode.GC.Co -@[deprecated "c ∈ Unicode.GC.Co" (since := "1.2.0")] -protected abbrev isCo := isPrivateUse - /-- Check if unassigned character (`Cn`) Unicode Property: `General_Category=Cn` -/ abbrev isUnassigned (char : Char) : Bool := char ∈ Unicode.GC.Cn -@[deprecated "c ∈ Unicode.GC.Cn" (since := "1.2.0")] -protected abbrev isCn := isUnassigned - end GeneralCategory /-! diff --git a/UnicodeBasic/TableLookup.lean b/UnicodeBasic/TableLookup.lean index 14c3dc597..bf66cc859 100644 --- a/UnicodeBasic/TableLookup.lean +++ b/UnicodeBasic/TableLookup.lean @@ -180,11 +180,6 @@ where @[inline] def lookupGC (c : UInt32) : GC := CLib.lookupProp c |>.toUInt32 -set_option linter.deprecated false in -@[inline, deprecated Unicode.lookupGC (since := "v1.3.0")] -def lookupGeneralCategory (c : UInt32) : GeneralCategory := - .ofGC! (lookupGC c) - /-- Get name of a code point using lookup table Unicode property: `Name` -/ diff --git a/UnicodeBasic/Types.lean b/UnicodeBasic/Types.lean index 5dff2605a..f3b863de4 100644 --- a/UnicodeBasic/Types.lean +++ b/UnicodeBasic/Types.lean @@ -467,249 +467,6 @@ def ofString! (s : String.Slice) : GC := end GC -set_option linter.deprecated false in -@[deprecated Unicode.GC (since := "1.2.0")] -structure GeneralCategory : Type where - /-- Major general category of a code point -/ - major : MajorGeneralCategory - /-- Minor general category of a code point -/ - minor : Option (MinorGeneralCategory major) -deriving Inhabited, DecidableEq - -set_option linter.deprecated false in section - -/-- General category: letter (`L`) -/ -@[deprecated Unicode.GC.L (since := "1.2.0")] -protected def GeneralCategory.L : GeneralCategory := ⟨.letter, none⟩ -/-- General category: cased letter (`LC`) -/ -@[deprecated Unicode.GC.LC (since := "1.2.0")] -protected def GeneralCategory.LC : GeneralCategory := ⟨_, some .casedLetter⟩ -/-- General category: uppercase letter (`Lu`) -/ -@[deprecated Unicode.GC.Lu (since := "1.2.0")] -protected def GeneralCategory.Lu : GeneralCategory := ⟨_, some .uppercaseLetter⟩ -/-- General category: lowercase letter (`Ll`) -/ -@[deprecated Unicode.GC.Ll (since := "1.2.0")] -protected def GeneralCategory.Ll : GeneralCategory := ⟨_, some .lowercaseLetter⟩ -/-- General category: titlecase letter (`Lt`) -/ -@[deprecated Unicode.GC.Lt (since := "1.2.0")] -protected def GeneralCategory.Lt : GeneralCategory := ⟨_, some .titlecaseLetter⟩ -/-- General category: modifier letter (`Lm`) -/ -@[deprecated Unicode.GC.Lm (since := "1.2.0")] -protected def GeneralCategory.Lm : GeneralCategory := ⟨_, some .modifierLetter⟩ -/-- General category: other letter (`Lo`) -/ -@[deprecated Unicode.GC.Lo (since := "1.2.0")] -protected def GeneralCategory.Lo : GeneralCategory := ⟨_, some .otherLetter⟩ -/-- General category mark (`M`) -/ -@[deprecated Unicode.GC.M (since := "1.2.0")] -protected def GeneralCategory.M : GeneralCategory := ⟨.mark, none⟩ -/-- General category: nonspacing combining mark (`Mn`) -/ -@[deprecated Unicode.GC.Mn (since := "1.2.0")] -protected def GeneralCategory.Mn : GeneralCategory := ⟨_, some .nonspacingMark⟩ -/-- General category: spacing combining mark (`Mc`) -/ -@[deprecated Unicode.GC.Mc (since := "1.2.0")] -protected def GeneralCategory.Mc : GeneralCategory := ⟨_, some .spacingMark⟩ -/-- General category: enclosing combining mark (`Me`) -/ -@[deprecated Unicode.GC.Me (since := "1.2.0")] -protected def GeneralCategory.Me : GeneralCategory := ⟨_, some .enclosingMark⟩ -/-- General category: number (`N`) -/ -@[deprecated Unicode.GC.N (since := "1.2.0")] -protected def GeneralCategory.N : GeneralCategory := ⟨.number, none⟩ -/-- General category: decimal digit (`Nd`) -/ -@[deprecated Unicode.GC.Nd (since := "1.2.0")] -protected def GeneralCategory.Nd : GeneralCategory := ⟨_, some .decimalNumber⟩ -/-- General category: letter number (`Nl`) -/ -@[deprecated Unicode.GC.Nl (since := "1.2.0")] -protected def GeneralCategory.Nl : GeneralCategory := ⟨_, some .letterNumber⟩ -/-- General category: other number (`No`) -/ -@[deprecated Unicode.GC.No (since := "1.2.0")] -protected def GeneralCategory.No : GeneralCategory := ⟨_, some .otherNumber⟩ -/-- General category: punctuation (`P`) -/ -@[deprecated Unicode.GC.P (since := "1.2.0")] -protected def GeneralCategory.P : GeneralCategory := ⟨.punctuation, none⟩ -/-- General category: connector punctuation (`Pc`) -/ -@[deprecated Unicode.GC.Pc (since := "1.2.0")] -protected def GeneralCategory.Pc : GeneralCategory := ⟨_, some .connectorPunctuation⟩ -/-- General category: dash punctuation (`Pd`) -/ -@[deprecated Unicode.GC.Pd (since := "1.2.0")] -protected def GeneralCategory.Pd : GeneralCategory := ⟨_, some .dashPunctuation⟩ -/-- General category: grouping punctuation (`PG`) -/ -@[deprecated Unicode.GC.PG (since := "1.2.0")] -protected def GeneralCategory.PG : GeneralCategory := ⟨_, some .groupPunctuation⟩ -/-- General category: opening punctuation (`Ps`) -/ -@[deprecated Unicode.GC.Ps (since := "1.2.0")] -protected def GeneralCategory.Ps : GeneralCategory := ⟨_, some .openPunctuation⟩ -/-- General category: closing punctuation (`Pe`) -/ -@[deprecated Unicode.GC.Pe (since := "1.2.0")] -protected def GeneralCategory.Pe : GeneralCategory := ⟨_, some .closePunctuation⟩ -/-- General category: quoting punctuation (`PQ`) -/ -@[deprecated Unicode.GC.PQ (since := "1.2.0")] -protected def GeneralCategory.PQ : GeneralCategory := ⟨_, some .quotePunctuation⟩ -/-- General category: initial punctuation (`Pi`) -/ -@[deprecated Unicode.GC.Pi (since := "1.2.0")] -protected def GeneralCategory.Pi : GeneralCategory := ⟨_, some .initialPunctuation⟩ -/-- General category: final punctuation (`Pf`) -/ -@[deprecated Unicode.GC.Pf (since := "1.2.0")] -protected def GeneralCategory.Pf : GeneralCategory := ⟨_, some .finalPunctuation⟩ -/-- General category: other punctuation (`Po`) -/ -@[deprecated Unicode.GC.Po (since := "1.2.0")] -protected def GeneralCategory.Po : GeneralCategory := ⟨_, some .otherPunctuation⟩ -/-- General category: symbol (`S`) -/ -@[deprecated Unicode.GC.S (since := "1.2.0")] -protected def GeneralCategory.S : GeneralCategory := ⟨.symbol, none⟩ -/-- General category: math symbol (`Sm`) -/ -@[deprecated Unicode.GC.Sm (since := "1.2.0")] -protected def GeneralCategory.Sm : GeneralCategory := ⟨_, some .mathSymbol⟩ -/-- General category: currency symbol (`Sc`) -/ -@[deprecated Unicode.GC.Sc (since := "1.2.0")] -protected def GeneralCategory.Sc : GeneralCategory := ⟨_, some .currencySymbol⟩ -/-- General category: modifier symbol (`Sk`) -/ -@[deprecated Unicode.GC.Sk (since := "1.2.0")] -protected def GeneralCategory.Sk : GeneralCategory := ⟨_, some .modifierSymbol⟩ -/-- General category: other symbol (`So`) -/ -@[deprecated Unicode.GC.So (since := "1.2.0")] -protected def GeneralCategory.So : GeneralCategory := ⟨_, some .otherSymbol⟩ -/-- General category: separator (`Z`) -/ -@[deprecated Unicode.GC.Z (since := "1.2.0")] -protected def GeneralCategory.Z : GeneralCategory := ⟨.separator, none⟩ -/-- General category: space separator (`Zs`) -/ -@[deprecated Unicode.GC.Zs (since := "1.2.0")] -protected def GeneralCategory.Zs : GeneralCategory := ⟨_, some .spaceSeparator⟩ -/-- General category: line separator (`Zl`) -/ -@[deprecated Unicode.GC.Zl (since := "1.2.0")] -protected def GeneralCategory.Zl : GeneralCategory := ⟨_, some .lineSeparator⟩ -/-- General category: paragraph separator (`Zp`) -/ -@[deprecated Unicode.GC.Zp (since := "1.2.0")] -protected def GeneralCategory.Zp : GeneralCategory := ⟨_, some .paragraphSeparator⟩ -/-- General category: other (`C`) -/ -@[deprecated Unicode.GC.C (since := "1.2.0")] -protected def GeneralCategory.C : GeneralCategory := ⟨.other, none⟩ -/-- General category: control (`Cc`) -/ -@[deprecated Unicode.GC.Cc (since := "1.2.0")] -protected def GeneralCategory.Cc : GeneralCategory := ⟨_, some .control⟩ -/-- General category: format (`Cf`) -/ -@[deprecated Unicode.GC.Cf (since := "1.2.0")] -protected def GeneralCategory.Cf : GeneralCategory := ⟨_, some .format⟩ -/-- General category: surrogate (`Cs`) -/ -@[deprecated Unicode.GC.Cs (since := "1.2.0")] -protected def GeneralCategory.Cs : GeneralCategory := ⟨_, some .surrogate⟩ -/-- General category: private use (`Co`) -/ -@[deprecated Unicode.GC.Co (since := "1.2.0")] -protected def GeneralCategory.Co : GeneralCategory := ⟨_, some .privateUse⟩ -/-- General category: unassigned (`Cn`) -/ -@[deprecated Unicode.GC.Cn (since := "1.2.0")] -protected def GeneralCategory.Cn : GeneralCategory := ⟨_, some .unassigned⟩ - -def GeneralCategory.toGC : GeneralCategory → GC -| ⟨.letter, none⟩ => .L -| ⟨_, some .casedLetter⟩ => .LC -| ⟨_, some .uppercaseLetter⟩ => .Lu -| ⟨_, some .lowercaseLetter⟩ => .Ll -| ⟨_, some .titlecaseLetter⟩ => .Lt -| ⟨_, some .modifierLetter⟩ => .Lm -| ⟨_, some .otherLetter⟩ => .Lo -| ⟨.mark, none⟩ => .M -| ⟨_, some .nonspacingMark⟩ => .Mn -| ⟨_, some .spacingMark⟩ => .Mc -| ⟨_, some .enclosingMark⟩ => .Me -| ⟨.number, none⟩ => .N -| ⟨_, some .decimalNumber⟩ => .Nd -| ⟨_, some .letterNumber⟩ => .Nl -| ⟨_, some .otherNumber⟩ => .No -| ⟨.punctuation, none⟩ => .P -| ⟨_, some .connectorPunctuation⟩ => .Pc -| ⟨_, some .dashPunctuation⟩ => .Pd -| ⟨_, some .groupPunctuation⟩ => .PG -| ⟨_, some .openPunctuation⟩ => .Ps -| ⟨_, some .closePunctuation⟩ => .Pe -| ⟨_, some .quotePunctuation⟩ => .PQ -| ⟨_, some .initialPunctuation⟩ => .Pi -| ⟨_, some .finalPunctuation⟩ => .Pf -| ⟨_, some .otherPunctuation⟩ => .Po -| ⟨.symbol, none⟩ => .S -| ⟨_, some .mathSymbol⟩ => .Sm -| ⟨_, some .currencySymbol⟩ => .Sc -| ⟨_, some .modifierSymbol⟩ => .Sk -| ⟨_, some .otherSymbol⟩ => .So -| ⟨.separator, none⟩ => .Z -| ⟨_, some .spaceSeparator⟩ => .Zs -| ⟨_, some .lineSeparator⟩ => .Zl -| ⟨_, some .paragraphSeparator⟩ => .Zp -| ⟨.other, none⟩ => .C -| ⟨_, some .control⟩ => .Cc -| ⟨_, some .format⟩ => .Cf -| ⟨_, some .surrogate⟩ => .Cs -| ⟨_, some .privateUse⟩ => .Co -| ⟨_, some .unassigned⟩ => .Cn - -@[deprecated some (since := "1.2.0")] -def GeneralCategory.ofGC? (c : GC) : Option GeneralCategory := - if c == .C then some .C else - if c == .Cc then some .Cc else - if c == .Cf then some .Cf else - if c == .Cs then some .Cs else - if c == .Co then some .Co else - if c == .Cn then some .Cn else - if c == .L then some .L else - if c == .LC then some .LC else - if c == .Lu then some .Lu else - if c == .Ll then some .Ll else - if c == .Lt then some .Lt else - if c == .Lm then some .Lm else - if c == .Lo then some .Lo else - if c == .M then some .M else - if c == .Mn then some .Mn else - if c == .Mc then some .Mc else - if c == .Me then some .Me else - if c == .N then some .N else - if c == .Nd then some .Nd else - if c == .Nl then some .Nl else - if c == .No then some .No else - if c == .P then some .P else - if c == .PG then some .PG else - if c == .PQ then some .PQ else - if c == .Pc then some .Pc else - if c == .Pd then some .Pd else - if c == .Ps then some .Ps else - if c == .Pe then some .Pe else - if c == .Pi then some .Pi else - if c == .Pf then some .Pf else - if c == .Po then some .Po else - if c == .S then some .S else - if c == .Sm then some .Sm else - if c == .Sc then some .Sc else - if c == .Sk then some .Sk else - if c == .So then some .So else - if c == .Z then some .Z else - if c == .Zs then some .Zs else - if c == .Zl then some .Zl else - if c == .Zp then some .Zp else - none - -@[deprecated id (since := "1.2.0")] -def GeneralCategory.ofGC! (c : GC) : GeneralCategory := - (ofGC? c).get! - -/-- String abbreviation for general category -/ -@[deprecated Unicode.GC.toAbbrev! (since := "1.2.0")] -def GeneralCategory.toAbbrev (c : GeneralCategory) : String := - c.toGC.toAbbrev! - -/-- Get general category from string abbreviation -/ -@[deprecated Unicode.GC.ofAbbrev? (since := "1.2.0")] -def GeneralCategory.ofAbbrev? (s : String.Slice) : Option GeneralCategory := - GC.ofAbbrev? s >>= ofGC? - -@[deprecated Unicode.GC.ofAbbrev! (since := "1.2.0"), inherit_doc GeneralCategory.ofAbbrev?] -def GeneralCategory.ofAbbrev! (s : String.Slice) : GeneralCategory := - match ofAbbrev? s with - | some gc => gc - | none => panic! "invalid general category abbreviation" - -instance : Repr GeneralCategory where - reprPrec gc _ := s!"Unicode.GeneralCategory.{gc.toAbbrev}" - -end - /-! ## Numeric Type and Value ## -/ diff --git a/UnicodeData/Basic.lean b/UnicodeData/Basic.lean index 301079d02..20b06e55f 100644 --- a/UnicodeData/Basic.lean +++ b/UnicodeData/Basic.lean @@ -49,34 +49,6 @@ structure UnicodeData where titlecase : Option Char := none deriving BEq -@[deprecated UnicodeData.code (since := "1.2.0")] -abbrev UnicodeData.codeValue := @UnicodeData.code - -@[deprecated UnicodeData.name (since := "1.2.0")] -abbrev UnicodeData.characterName := @UnicodeData.name - -set_option linter.deprecated false in -@[deprecated UnicodeData.gc (since := "1.2.0")] -def UnicodeData.generalCategory (d : UnicodeData) : GeneralCategory := .ofGC! d.gc - -@[deprecated UnicodeData.bidi (since := "1.2.0")] -abbrev UnicodeData.bidiClass := @UnicodeData.bidi - -@[deprecated UnicodeData.cc (since := "1.2.0")] -abbrev UnicodeData.canonicalCombiningClass := @UnicodeData.cc - -@[deprecated UnicodeData.cc (since := "1.2.0")] -abbrev UnicodeData.decompositionMapping := @UnicodeData.decomp - -@[deprecated UnicodeData.lowercase (since := "1.2.0")] -abbrev UnicodeData.lowercaseMapping := @UnicodeData.lowercase - -@[deprecated UnicodeData.uppercase (since := "1.2.0")] -abbrev UnicodeData.uppercaseMapping := @UnicodeData.uppercase - -@[deprecated UnicodeData.titlecase (since := "1.2.0")] -abbrev UnicodeData.titlecaseMapping := @UnicodeData.titlecase - instance : Inhabited UnicodeData where default := { code := 0