got a basic "info panel" working. it shows the local assumptions and the current goal (at the cursor).
as in my previous demo, the first example shows using the rw tactic to use theorems to rewrite the goal into the form x = x, which is trivally true.
the second example shows unfolding definitions (negation is defined as P -> False) and introducing assumptions.
sadly, i only had two days to work on the project this week (so i didn't really get to the "interactivity" i had hoped for). still it was a lot of fun and i learned a couple of things 👌 &kibi-pa