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.

Sign up for GitHub

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

Jump to bottom

Review essential tutorial content #135

Open
wants to merge 13 commits into
base: main
Choose a base branch
from
Open

Review essential tutorial content #135

wants to merge 13 commits into from

Conversation

jonaprieto
Copy link
Collaborator

@jonaprieto jonaprieto commented Dec 23, 2024 •
edited
Loading

Markdown formatting improvements and a few text refinements.

@jonaprieto
Copy link
Collaborator Author

jonaprieto commented Dec 23, 2024 •
edited
Loading

Success! The preview of this PR will be available at https://docs.juvix.org/pull-135/ in a few minutes.

Please note that this link will be deleted when the PR is closed or merged.

@jonaprieto jonaprieto changed the title read until Local definitions Proof-read essential tutorial Dec 23, 2024
@jonaprieto jonaprieto changed the title Proof-read essential tutorial Review essential tutorial content Dec 25, 2024
@jonaprieto jonaprieto marked this pull request as ready for review December 25, 2024 15:02
@lukaszcz
Copy link
Contributor

Please revert line-break changes so that it is possible to see in the diff what was actually changed

@lukaszcz lukaszcz self-requested a review December 25, 2024 22:38
lukaszcz
lukaszcz reviewed Dec 25, 2024
View reviewed changes
docs/tutorials/essential.juvix.md

```juvix
foo (pair : Pair Nat Nat) : Nat :=
let
(x, y) := pair;
bar := 42 + y;
bar : Nat := 42 + y;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was intentionally without type here, to show that you can omit it (and this is mentioned in the paragraph below).

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I noticed, read the text after this code block.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay, so why do you think the Nat should be there?

Copy link
Collaborator Author

@jonaprieto jonaprieto Jan 13, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Even though you mentioned that those type annotations are permitted, I didn't see any example of that in the code examples. Maybe I missed something. I usually skim through the code examples; after that, I read the text if needed.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is just above with myValue : Nat := ... True, not inside a let, but the paragraph mentions that the syntax is exactly the same as for top-level definitions, and proceeds to demonstrate definition syntax not shown before.

@jonaprieto
Copy link
Collaborator Author

jonaprieto commented Dec 29, 2024 •
edited
Loading

Success! The preview of this PR will be available at https://docs.juvix.org/pull-135/ in a few minutes.

Please note that this link will be deleted when the PR is closed or merged.

@lukaszcz lukaszcz force-pushed the jonathan/proof-read branch from 8fb602f to 260b32b Compare January 7, 2025 10:48
@lukaszcz lukaszcz self-requested a review January 13, 2025 09:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lukaszcz lukaszcz Awaiting requested review from lukaszcz

Assignees

@jonaprieto jonaprieto

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@jonaprieto @lukaszcz