Hello.
The video has no sound (that way, I won't have to record it again if I
mess up the comments).
When/If the app becomes useful, I'll publish the app and video/tutorial
with sounds to explain features/workflow.
At this point, the video is mostly there so that we can discuss what
would be a nicer UI/way of doing things,
what we can accomplish and what we cannot, possibilities, features,
wishes, etc...
Obviously, making the action menu resizable and dragable was a big
mistake : next time, it'll be anchored at the right side of the window
and will resize automatically automatically
Also, past mutations will be foldable/hidden, so that they don't take
too much screen estate and so that we can concentrate on the last result
The "select and mutate" process is the signature move of Mephistolus at
this point.
It is also available in 2 of mutation categories :
same "power" equality =, equivalence <->
different "power" : implication ->, inequalities <=, <, binary relations...
For example :
|- ( x in A -> x <_ 2 )
with the mutation
|- 2 <_ 3
provides |- ( x in A -> x <_ 3 ) by proving the statement |- ( x in A ->
( x <_ 2 ) -> x <_ 3 ) )
Different "power"
Olivier
Le 22/01/2020 à 10:00, Giovanni Mascellani a écrit :
Hi,
Il 21/01/20 22:24, Olivier Binda ha scritto:
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 ^^;
Nice video, it seems to be a useful tool for this type of computations.
Being able to visually select and manipulate an expression can be
convenient to locally edit a formula while at the same time having a
global view on the whole of it.
Does the vieo have a comment? To me the video is completely mute (I can
hear the audio from other YouTube videos, so it doesn't seem to be a
problem in my gear).
Giovanni.
--
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/9c55c01a-00dc-6cf4-8966-b3a2f1d46e06%40gmail.com.
