structure Unicode.Emoji : Type

• name : String
• properties : Array (UInt32 × Option UInt32)

instance Unicode.instToStringEmoji : ToString Unicode.Emoji

Equations

• Unicode.instToStringEmoji = { toString := fun (s : Unicode.Emoji) => toString "" ++ toString s.name ++ toString " " ++ toString s.properties ++ toString "" }

def Unicode.Emojis.txt : String

Equations

• One or more equations did not get rendered due to their size.

def Unicode.Emojis.data : Array Unicode.Emoji

Equations

• Unicode.Emojis.data = #[]

def Unicode.getEmoji (s : String) : Except String (Array (NonemptyInterval Char))

Equations

• One or more equations did not get rendered due to their size.