The EMetamath plugin for Ecplise

71 views
Skip to first unread message

Thierry Arnoux

unread,
Dec 6, 2020, 9:18:35 AM12/6/20
to metamath

Hi all,

Since there were recently discussions about the features one would wish of a proof assistant GUI for Metamath, I've recorded a (long overdue) video showing the features I've implemented over time in the EMetamath plugin for Eclipse:

https://youtu.be/BsEyW3vBcsE

I hope you find it interesting!
This was my first take, pardon the hesitations and my terrible accent! ;-)
_
Thierry


Jim Kingdon

unread,
Dec 6, 2020, 12:39:37 PM12/6/20
to Thierry Arnoux, metamath
Very nice. Gives a good feel for what EMetamath can do. And the accent was very understandable, at least to my ears, so no worries about that.

drjonp...@gmail.com

unread,
Dec 6, 2020, 5:29:31 PM12/6/20
to Metamath
Yeah I think this is really cool, there are a lot of nice features there, almost everything you pointed out I said "oh yeah that's sp helpful!"

Also your accent is really classy, love it.

David A. Wheeler

unread,
Dec 6, 2020, 6:17:20 PM12/6/20
to Metamath Mailing List
I thought this video was great! I didn’t have any trouble understanding you.

I think you should make it public & create links to it!!

--- David A. Wheeler

Glauco

unread,
Dec 6, 2020, 6:54:05 PM12/6/20
to Metamath
Really nice.

Thierry, you have shown the recently added feature

option+shift+rightArrow selection

in the source file. Does it also work in proof files? (I really wish mmj2 had this feature)

Thanks again for your nice video.


Glauco

Thierry Arnoux

unread,
Dec 6, 2020, 10:09:19 PM12/6/20
to meta...@googlegroups.com
> Le 7 déc. 2020 à 07:54, Glauco <glaform...@gmail.com> a écrit :
>
>  Does it also work in proof files?

Yes it does! Actually this is where it is most useful and where I use it most of the time, I really shall have shown it in that editor.


Reply all
Reply to author
Forward
0 new messages