Reservoir

xubaiw/Unicode.lean

Unicode stuff for Lean 4! ✌️

GitHub Link Documentation

Pick a version!

TODO: should show a time axes that allows the users to view, filter and click copy the lakefile config.

README

Unicode.lean

Unicode related operations for Lean 4.

  • Unicode General Category
  • TODO

NOTE: As Unicode is a huge specification, it will take a long time to implement all its features. If you feel some feature is more urgent, feel free to open an issue or a pull request!

Installation

In your lakefile.lean add Unicode.lean as dependency:

package foo {
  dependencies := #[{
    name := `Unicode
    src := Source.git "https://github.com/xubaiw/Unicode.lean" "main" 
  }]
}

Usage

The following example shows how to get general category propert of a character:

import Unicode.General.GeneralCategory
open Unicode

#eval getGeneralCategory 'a' -- Ll, lowercase letter
#eval getGeneralCategory '←' -- Sm, math symbol
#eval getGeneralCategory '-' -- Pd, dash punctuation
#eval getGeneralCategory $ Char.mk 0x10ead (by decide) -- Pd, dash punctuation

More examples can be found in the examples folder, and the documentation is redered through doc-gen4.