search

digama0 / mm0

Metamath Zero specification language
Creative Commons Zero v1.0 Universal
306 stars 40 forks source link

improve tutorial #96

Closed tlyu closed 2 years ago

tlyu commented 2 years ago

Add comments to tutorial files so they're easier to follow without watching the video. Add timestamps from the video to the README. Add some usages with debugging to demystify the conj-prove examples.

benjub commented 2 years ago

Thanks @tlyu, that's useful ! Why "--|" instead of "--" in somme comments ?

tlyu commented 2 years ago

Thanks @tlyu, that's useful ! Why "--|" instead of "--" in somme comments ?

The --|is a doc comment that adds to the annotations shown when hovering a use of an item. https://github.com/digama0/mm0/blob/master/mm0-hs/mm1.md#doc-comments

tlyu commented 2 years ago

Thanks for the review! I applied your suggestions.