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

Review essential tutorial content #135

Merged
merged 15 commits into from
Jan 14, 2025
Merged

Review essential tutorial content #135

merged 15 commits into from
Jan 14, 2025

Conversation

jonaprieto
Copy link
Collaborator

@jonaprieto jonaprieto commented Dec 23, 2024

Markdown formatting improvements and a few text refinements.

@jonaprieto
Copy link
Collaborator Author

jonaprieto commented Dec 23, 2024

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


```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

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

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.

@@ -738,14 +962,17 @@ dividePrice (n : Nat) (r : Resource) : Resource :=
};
```


## Common techniques
Copy link
Contributor

Choose a reason for hiding this comment

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

The edits in this section messed up the formatting of lists (some sublists not correctly indented) and Juvix code blocks (some moved to the very left, others remained indented as before). This needs to be fixed.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

huh! I didn't notice that.
Anyway, I think they are fixed now.

Copy link
Contributor

Choose a reason for hiding this comment

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

No, it didn't work. The sublists are not indented. I don't know how to fix this other than removing the sublists.

Copy link
Contributor

Choose a reason for hiding this comment

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

I removed the sublists. Tried to keep the headings as comments inside the code, but unfortunately Juvix markdown processing currently removes comments.

@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
@lukaszcz lukaszcz merged commit e831d99 into main Jan 14, 2025
1 check passed
@lukaszcz lukaszcz deleted the jonathan/proof-read branch January 14, 2025 12:15
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.

2 participants