Luna Tuna (Oct 05 2020 at 21:53): Luna Tuna (Oct 05 2020 at 21:53):I'm googling around trying to figure out how to do this. There's no information on it. I want to enter in B_0 for example where _0 means subscripted 0.
Jasper Hugunin (Oct 05 2020 at 22:05):You may be looking for https://github.com/coq/coq/wiki/CoqIde-configuration-to-input-special-characters, in general you need a way to type unicode characters. That can be copy-paste, an OS specific method, or something else.
Jasper Hugunin (Oct 05 2020 at 22:08):I personally am running CoqIDE on WSL+Ubuntu through an X window server, and I use the uim input method to type unicode characters. That is however a somewhat uncommon setup, so it may not be applicable to your situation.
Luna Tuna (Oct 05 2020 at 22:34):Jasper Hugunin said:
You may be looking for https://github.com/coq/coq/wiki/CoqIde-configuration-to-input-special-characters, in general you need a way to type unicode characters. That can be copy-paste, an OS specific method, or something else.
There seems to be no easy way to do this on Windows 10 from the keyboard. So I guess the solution is to use the JsCoq scratchpad in the browser.
Note to anyone in the future. The best way in JsCoq to enter in a subscript is to type in a double-underscore. It then switches modes to subcript and you can type anything.
Théo Zimmermann (Oct 06 2020 at 07:42):Since Coq 8.10, CoqIDE embeds its own input method. See https://coq.inria.fr/refman/practical-tools/coqide.html#bindings-for-input-of-unicode-symbols. You can get a subscript 0 with \_0.
Last updated: Sep 30 2023 at 06:01 UTC