they now have a turnkey tool to display complex visualizations in the infoview https://github.com/EdAyers/ProofWidgets4. in your view, is this useful for coq users? my opinion is i like the idea, but I'm skeptical of its usefulness
probably useful in teaching and documentation, most obviously together with Alectryon
Wouldn't it be useful for a CAS-like application?
i dont get what you mean :)
From their README
We have good support for building diagrams with Penrose, and expose some Recharts components for plotting functions and other kinds of data.
Seems useful for plotting functions like CAS (computer-algebra systems) do, Coq has libraries for doing it correctly
alternative and domain-specific goal state displays
That describes proof modes for custom embedded logics like Iris, I definitely refuse to stick to pen and paper for that
Your post seems to say that this library can be misused. I'm sure that's true, I'm less sure we'll actually write so much bad code.
for verified plotting, there are no less than two different solutions in Coq: https://coq.discourse.group/t/interval-4-2-now-with-plotting/1248
yes, I was thinking of that; such widgets might have UX upsides over "run gnuplot"
Last updated: Nov 29 2023 at 22:01 UTC