I agree with Marnix that you should just pre-fix the tutorial pages rather than talking about how the tutorial is out of date in the video. Also, on page 303 you forgot to put "200,1000" in for step qed. (But it would be more impressive if you put a ! at the start, as in "!qed" with nothing else, and then it will figure out *both* the hyps and the ref. But that is a feature added after the tutorial was written.)
The transition from page 404 to 405 is incorrect, because the derive steps now have a different format, namely !d1:: rather than 1000:?: . Again this is a place where the tutorial should be fixed rather than talking around it. In addition, I would recommend using "!step::" for incomplete steps rather than "step:?:", as the bang will cause it to try to passively justify it on every unify (meaning that unrelated steps can sometimes get proven while you are working on something else), and the ? is no longer necessary to indicate "incomplete hyps" and will interfere with unification (as indicated, it doesn't try to unify these steps). I would have completely removed the "?" but it breaks a lot of backward compatibility. It is currently only useful for the "step search": if you double click on "step:: |- foo" then it will search only for proofs of |- foo with no assumptions, and if you double click "step:?: |- foo" it will search for proofs of foo with possibly additional hypotheses. On page 411, it might be worth mentioning that you can also write "#" instead of "#1" and it will search for any matching step. If you use this form it will only search previous steps, but the #1 form will also work if it is a forward reference, and it will check that you aren't creating a cycle and reorder all the steps so that references are topologically sorted. On Wed, Jan 8, 2020 at 6:44 AM Jon P <[email protected]> wrote: > > Hi David, very nice tutorial, I learned a lot of interesting things. > > Re the sound quality I think maybe you are a bit close to your mic, you > are getting a bit of breathing coming through and popping on p sounds. > However it isn't a big deal and wasn't particularly noticeable. > > You say in some places, like in file 302, that things have changed since > the tutorial was written and it is a bit outdated, such as it now needing > more :'s. Do you think it is worth updating the tutorial files when you > found these? > > For me the most useful feature of mmj2 is putting an ! at the beginning of > the line, this seems to magically fill in everything for me which is very > nice. It seems this did not come up in the tutorial and it's the first > thing I would tell people ha ha. > > Overall very nice, thanks for making it. > > Jon > > > > -- > 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/175830c6-3ad4-4460-a2a2-da743f902220%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/175830c6-3ad4-4460-a2a2-da743f902220%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/CAFXXJSvyNHFWTsH6GrkYxj%2BHDF3UpStmr9cL6mKZ5VHj%3DcO_zA%40mail.gmail.com.
