Stream: Coq users

Topic: How do you enter in a subscript in Coq IDE?


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Feb 06 2023 at 13:03 UTC