Maxime Dénès (Jun 02 2020 at 08:31): Maxime Dénès (Jun 02 2020 at 08:31):@Emilio Jesús Gallego Arias by any chance, did you write a piece of code which renders Pp.t to HTML, in one of your projects? It would be useful for the goal display in VsCoq.
Emilio Jesús Gallego Arias (Jun 02 2020 at 11:37):Best candidate, but not yet 100% perfect is Shachar's code in jsCoq
Maxime Dénès (Jun 02 2020 at 11:46):Do you have a pointer to the code?
Maxime Dénès (Jun 02 2020 at 11:48):Ok, I guess I can have a look at https://github.com/jscoq/jscoq/blob/v8.11/ui-js/format-pprint.js
Emilio Jesús Gallego Arias (Jun 02 2020 at 11:48):https://github.com/jscoq/jscoq/blob/v8.11/ui-js/format-pprint.js
Emilio Jesús Gallego Arias (Jun 02 2020 at 11:48):yup that is
Maxime Dénès (Jun 02 2020 at 11:50):thanks
Last updated: Oct 13 2024 at 01:02 UTC