Unicode notation question

Stream: new members

[Ching-Tsun Chou]

I would like to introduce a postfix notation like what's shown below. But instead of ^ω, what I really want is a superscript ω, similar to the notation for set complementation which is a superscript c. But I don't know how to achieve that. In particular, I don't know (1) how to get that unicode character and (2) how to define the key binding for producing that character in VScode. I'd appreciate any pointer to how to do these goals.

@[notation_class]
class OmegaPower (α : Type*) (β : outParam (Type*)) where
  omegaPower : α → β

postfix:1024 "^ω" => OmegaPower.omegaPower

[Markus Himmel]

According to Wikipedia, the only Greek superscript letters that are available in Unicode are ᵝᵞᵟᵠᵡᶿ, so you might be out of luck.

[Ching-Tsun Chou]

OK. I guess I'm out of luck then.

[Ching-Tsun Chou]

On the other hand, maybe I can use the superscript version of Latin W or w? Also, there is something in "Unified Canadian Aboriginal Syllabics" that looks awfully like an omega superscript: ᐜ. Perhaps I can use one of them?

[Ching-Tsun Chou]

Unfortunately, the Latin W and w don't look good and don't really resemble the Greek ω as a superscript. Is the Lean key bindings for Unicode characters a feature of VScode and Emacs, or a part of Lean itself? If the latter is the case, then I can consider using that funny symbol ᐜ from "Unified Canadian Aboriginal Syllabics". If not, then I guess the current ^ω will have to be used.

[Robin Arnez]

I've seen people add abbreviations for VS code; I assume something similar can be used for Emacs and Neovim

[Ching-Tsun Chou]

If those key bindings are not part of Lean itself but have to be defined separately in various editors/IDEs, then I'd rather not use them.

[Robin Arnez]

Well they are in the @leanprover/unicode-input-component package

[Robin Arnez]

(https://github.com/leanprover/vscode-lean4/tree/master/lean4-unicode-input-component)

[Robin Arnez]

Oh but yeah you can't (I don't think) add them through meta-programming