Yup, I'll publish it once I get all the basic features working. The next one on my list is a proper block palette; right now it's just some hardcoded templates. Once I get that, along with automatic workvar names and the ability to save theorems, I'll publish a live version. I still have plenty of plans for after that, but that will be enough to play around with. On Saturday, January 9, 2021 at 11:25:34 AM UTC-6 [email protected] wrote:
> Wow, this looks amazing. Do you plan on publishing it on GitHub or > something during development when you are done? > > [email protected] schrieb am Samstag, 9. Januar 2021 um 06:12:01 UTC+1: > >> Hello, >> >> I'm experimenting with using visual blocks to represent and edit proofs >> using the morphic.js framework by Jens Mönig >> <https://github.com/jmoenig/morphic.js>. I don't have a whole lot at the >> moment, but here's a screenshot of a nearly-complete proof of ( -. p -> ( p >> -> q ) ) from axioms to demonstrate what I have so far: >> >> [image: image.png] >> >> Each block represents a theorem. The slots represent mandatory >> hypotheses, and the block itself exposes the theorem's assertion. For this >> picture, I color-coded ax-1 as red, ax-2 as green, and ax-3 as blue. All >> blocks will unify their expressions when connected to a slot, updating >> their own label to match the new expression. >> >> The lowest block is just a pass-through block that exposes a "wff" slot >> in addition to the "|-" slot. It's used here to give the wff variables >> names, since they would otherwise just show up as "?" (like in the >> disconnected red block). >> >> This project is still very early in development, but I hope that it will >> become an intuitive way to experiment with theorem proving. >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/88dc0f7b-67cd-4af2-8c9d-a9b5bff19bc8n%40googlegroups.com.
