Could one have coqdoc comments in several languages and allow real-time switching between languages in a jsCoq interface? Would be interesting to have this beginner material available in this way: https://www.math.univ-paris13.fr/~rousselin/commencer_sujet.v
I'm thinking in the direction of annotating the source something like:
(**fr L'équivalence logique est notée en coq [<->].*) (**en Logical equivalence in Coq is written [<->].*)
That's a nice idea; in fact it feels like it would be a pity for this to be a jsCoq-only feature. If users invest the time and effort to write multilingual documents they would probably want coqdoc to also be able to generate outputs in multiple languages.
(or is this already a coqdoc feature that I am not aware of )
no, there is no feature like that in coqdoc to my knowledge. Maybe it could be more easily integrated into Alectryon? The reason for jsCoq is that one might use the browser language.
sure that sounds plausible. I wonder if at least there is an existing convention for those language tags.
jsCoq (and coq-lsp) support markdown natively (and LaTeX soon) so IMHO it would be sense to use existing facilities for these formats
Last updated: Jan 30 2023 at 17:03 UTC