Proof General is great, and emacs is quite capable of showing images.
Would there be any way of including images in literate Coq code?
Company-coq already replaces coq's ascii art by math-symbols.
Perhaps a similar thing is possible with symbol strings in comments. E.g.
(** Coq is great.
I don't know what the syntax should be. @Clément Pit-Claudel ?
Yup, it's very easy to include images in an Emacs buffer. You can do what you suggest with a font-lock rule. I can write an example if you want.
This topic was moved here from #User interfaces devs & users > Pictures in Proof General/emacs by Karl Palmskog
Last updated: Feb 06 2023 at 05:03 UTC