Updated video of "Introduction to Metamath-lamp, part 2"

[David A. Wheeler]

I have an updated version of the video "Introduction to Metamath-lamp, part 2":
https://youtu.be/WOp2xQ8mEE4
In this video I've improved the explanation around addition is associative, and also
added a demonstration that metamath-lamp's automation could have found it directly.

Last-minute comments welcome. It's currently unlisted;
I soon plan to switch it to "public".

Part 1 now has the last few useless seconds removed:
https://youtu.be/b-RfoUuQpAQ
and again, I plan to switch this from "unlisted" to "public" soon.

--- David A. Wheeler

[David Wheeler]

And finally, here's a draft of the video "Introduction to Metamath-lamp, part 3":
https://www.youtube.com/watch?v=Aqp3jAM2b60

This is the follow-on to:
"Introduction to Metamath-lamp, part 1" - https://youtu.be/b-RfoUuQpAQ
"Introduction to Metamath-lamp, part 2" - https://youtu.be/WOp2xQ8mEE4

I don't plan on making any more videos for a while, and unless someone tells me of some disaster, I' plan to turn these videos from "unlisted" to "public" in a day or so.

These are based on the guide I wrote, available here:
https://lamp-guide.metamath.org

--- David A. Wheeler

[Igor Ieskov]

Hi David,

All three parts are great. I have not found any issue.

BTW, I didn't know that hypotheses in the explorer are marked with such large circles in Firefox. In Chrome those circles are smaller. I will try to fix this.

-

Igor

[David A. Wheeler]

> On Jun 26, 2023, at 1:47 AM, Igor Ieskov wrote:
> Hi David,
> All three parts are great. I have not found any issue.

Thanks! Anyone who's interested in the full playlist of Metamath-lamp tutorials can go here:
https://www.youtube.com/playlist?list=PL1jSu6GGefBk3RhHW5Srpc2qxWMqhga9J

All: please "like" any of the videos if you liked them; that makes the Youtube algorithms happy.

> BTW, I didn't know that hypotheses in the explorer are marked with such large circles in Firefox. In Chrome those circles are smaller. I will try to fix this.

I wouldn't worry about it. It's distinct and that's what matters.

--- David A. Wheeler