Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

improve tutorial #96

Merged
merged 2 commits into from
Feb 10, 2022
Merged

improve tutorial #96

merged 2 commits into from
Feb 10, 2022

Conversation

tlyu
Copy link
Contributor

@tlyu tlyu commented Feb 10, 2022

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.

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
Copy link

benjub commented Feb 10, 2022

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

@tlyu
Copy link
Contributor Author

tlyu commented Feb 10, 2022

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

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@tlyu
Copy link
Contributor Author

tlyu commented Feb 10, 2022

Thanks for the review! I applied your suggestions.

@digama0 digama0 merged commit 91eacfb into digama0:master Feb 10, 2022
@tlyu tlyu deleted the improve-tutorial branch February 10, 2022 05:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants