Hi all,
FYI, I've added a few screenshots to the README file of the
metamath-vspa project <https://github.com/tirix/metamath-vspa>,
including one with an example of unification at the bottom of the page
(still work in progress..)
So I'm still slowly getting there...
BR,
_
Thierry
On 15/02/2022 10:40, Thierry Arnoux wrote:
Hi Glauco,
MMJ2-style unification is certainly a goal! Many building blocks for this are
actually already in place - not all, but we’re slowly getting there.
An even more remote goal would be to use this framework to build a more
tactics-based proof assistant, but that’s in a much more distant future!
Right now Metamath-knife’s API is still changing (and I expect it to continue).
One thing you’ll have to take care about if building metamath-vspa is to use
the correct version. I hope we fix that soon.
Any help is certainly welcome! The choice of Rust was discussed in this forum a
while ago, one motivation being that Ralph and Mario both master it. I’ve been
self-learning Rust, I still am not very good and I certainly still have a lot
to learn, but I had a lot of fun learning it. It has a lot of features I was
hoping for when programming in C.
Each editor function (diagnostics, completion, references, search, formatting,
etc.) is a different functionality which can be built in parallel and stay
relatively independent, so it shall be very feasible to have several people
working together on that project.
BR,
_
Thierry
Le 15 févr. 2022 à 03:54, Glauco<[email protected]> a écrit :
Thierry, this is so cool!
Is a mmj2 ctrl+u like action available? Please, feel free to ask if you need
help with this one (I don't know anything about Rust, but it's now on top of my
list of things to learn)
Can't wait to build and try it!
Glauco
--
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/8642c4eb-53a3-e436-150d-7e6e4764ce1b%40gmx.net.
