Zulip Chat Archive

Stream: general

Topic: Unicode input on android

Eric Wieser (Jun 02 2021 at 10:56):

I just found a neat trick for enabling a vs-code-like input method on android:

  1. Install https://play.google.com/store/apps/details?id=com.usr.dict.mgr&hl=en&gl=US. This asks for slightly scary permissions, since it's a keyboard; but you can remove them again after you're done
  2. Export your current "personal dictionary", just in case you want to be able to remove the thousands of lean "words"
  3. Import this dictionary: https://gist.github.com/eric-wieser/09b4c73bba4c130affec000ef44c333e
  4. Disable the permissions from UDM now that you're done the import
  5. Type \forall, and ∀ will appear as a suggestion above your mobile keyboard!

Damiano Testa (Jun 02 2021 at 11:49):

∀ ← ℝ

From my phone!

Johan Commelin (Jun 02 2021 at 11:54):

@Damiano Testa that doesn't typecheck :rofl:

Damiano Testa (Jun 02 2021 at 11:54):

Ahaha that's why I was seeing those red squiggles everywhere... :upside_down:

Huỳnh Trần Khanh (Jun 02 2021 at 13:36):

Thank you Eric! Now I can talk about the L∀∃N theorem prover on mobile using proper Unicode characters!

Eric Wieser orz :place_of_worship:

Last updated: Dec 20 2023 at 11:08 UTC