Very interesting!
It's nice to see that apart from entering the input at the very
beginning, and apart from the substitutions, you only deal with the
graphical display of the equations.
Do you have any idea how the last use of dummy variables (v1c, v3c), for
substitutions, could be eliminated?
I wonder what is the operation "order" towards the top of the list,
which results in "0". Does it mean it cannot be applied? Could you then
simply omit to list it?
Of course an interesting topic to discuss is the choice of when/where to
add parenthesis, we had an extensive discussion about this when I
introduced the
I saw some cases where it seems to be they can obviously be removed,
like in " ( k e. ( { A ... B } ) ) " at 2:10. That's parenthesis where
even set.mm does not have any! ;-)
On 22/01/2020 05:24, Olivier Binda wrote:
Mephisolus reached Milestone 6
Here is a video, proving that it did :
https://www.youtube.com/watch?v=HuLFpQxwkmU&feature=youtu.be
It shows me a bit stressed (this was my fith attempt, there is always
something going wrong... :) and struggling at the end with html ^^;
Sadly, the exported metamath proof had an issue (I store metamath
theorem with some renaming/shuhhling of variables and It messed up the
exported proof).
I'll fix it at soon as possible and hopefully post a valid exported
proof.
I'm quite happy with the result : it ended up a bit better that I
envisionned and, I already have quite a few ideas about how to further
enhance the user workflow and make it much better.
Hoping to get some feedback now :)
And preparing to start development of Mephistolus Milestone 7...
Best regards,
Olivier
--
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]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/af959f49-b997-48f3-9ae8-8705f04da967%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/af959f49-b997-48f3-9ae8-8705f04da967%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/42e3ea53-9a2d-d6d5-b176-93bf6f0f70c8%40gmx.net.
