Hey all, I was wondering if there was any way to use symbols as I would in TeX in a Coq file (note, I am not trying to just have my finished file have the symbols I want, I want specifically to type them, and see them in the file as I create it). Lean 3 comes to mind in terms of what I want to be able to do. In that I can type something like \Pi, and have it be replaced by that symbol.
You would need to patch VsCoq for that. If there are many folks who want this feature, we could implement it.
I'm an ex-Lean user. So far I haven't needed to type Unicode symbols in Coq because the ecosystem sticks to plain ASCII symbols. But if the community wants this feature, I'm willing to implement it.
There are already multiple Unicode Input extensions in the marketplace.. https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/editor.md#unicode-input-setup links to a configurable one with an example of configuration
jscoq does some beautiful things, @Emilio Jesús Gallego Arias probably has good insights on how to do literate proving across vscoq and jscoq. Or knows what the problems are...
I'm not sure whether markdown could be a complete replacement for tex/html which is currently used in coqdoc.
We had discussions like this in the past, the last being https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs-.26-users/topic/inputting.20UTF8.20symbols also you can use unicode notations in Coq by importing the
@Bas Spitters , indeed we are close to release new jsCoq version that will be "pure" literate, you can already input coq Markdown files in vscode using coq-lsp, but the schema is very basic.
Internally, we use a "schema", that is close to MyST Markdown , there is indeed the possibility to use TeX documents directly but I haven't looked into what TeX parser woud allow that. I would expect that format to replace coqdoc, but OMMV
Last updated: Jun 04 2023 at 22:30 UTC