Hi all,
This all sounds very interesting!
From the different posts, here is a possible breakdown I see:
* A "core" crate, (could it be based on smm3 ?), acting as a library
and providing services like:
o parsing and verifying metamath expressions and .mm files,
o listing theorems matching a given pattern,
o performing unitary steps like unification.
o manipulating proofs (adding a subgoal, adding a proof step,
declaring the proof complete)
* A "pa" (proof assistant) crate:
o parsing and executing the (possibly scheme-like) proof scripts
o giving real-time notifications to the UI
* Several "tactics" crates, written as plug-ins in Rust.
* A "ui" crate, handling everything UI related, e.g. based on Druid/Xi
Did I understand everything correctly?
I never tried rust, that could be an opportunity!
BR,
_
Thierry
--
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/a0cbb58a-ec83-08f7-f5b6-1f2c607b7c41%40gmx.net.
