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

Adding lesson on basic proofs #2699

Merged
merged 19 commits into from
Aug 6, 2022
Merged

Adding lesson on basic proofs #2699

merged 19 commits into from
Aug 6, 2022

Conversation

PetarMax
Copy link
Contributor

@PetarMax PetarMax commented Jul 4, 2022

Introducing Lesson 22 on basic proofs, using examples from the 0-to-K tutorial

@PetarMax PetarMax requested review from dwightguth and ehildenb July 4, 2022 07:14
@charala1
Copy link
Contributor

charala1 commented Jul 6, 2022

@PetarMax should we name the examples according to the lesson-22-* scheme as in the rest of the tutorial?

@PetarMax
Copy link
Contributor Author

PetarMax commented Jul 6, 2022

Yes, please, that naming convention should probably be respected.

@charala1
Copy link
Contributor

charala1 commented Jul 7, 2022

Yes, please, that naming convention should probably be respected.

Done. However, I think we should put the whole listings in as opposed to asking the reader to add definitions into the modules (and use lesson-22-{a, b, c...} prefixes for the various files). Maybe this is overkill, I don't know.

@PetarMax
Copy link
Contributor Author

PetarMax commented Jul 7, 2022

I'd prefer not to to present the entire file at once, because then I'd have to refer the reader back. Like this, it's all inlined in the text. Alternatively, the lesson itself could be the file, given literate programming. Perhaps that's the way to go?

@Baltoli
Copy link
Contributor

Baltoli commented Jul 8, 2022

See commands.sh for examples of how the tutorial's literate definitions are compiled in CI. You want each A, B, C module to be individually compilable with the appropriate setting for the main module.

@ehildenb ehildenb marked this pull request as ready for review August 2, 2022 20:57
@rv-jenkins rv-jenkins merged commit 86da689 into master Aug 6, 2022
@rv-jenkins rv-jenkins deleted the tutorial-lesson-22 branch August 6, 2022 05:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

8 participants