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