Skip to content

Remark on changing order of (m + n) to (n + m) in drop' in Section 6.3#88

Merged
stefan-hoeck merged 5 commits into
stefan-hoeck:mainfrom
Liable5607:added-remark-in-6.3
Jul 21, 2025
Merged

Remark on changing order of (m + n) to (n + m) in drop' in Section 6.3#88
stefan-hoeck merged 5 commits into
stefan-hoeck:mainfrom
Liable5607:added-remark-in-6.3

Conversation

@Liable5607

Copy link
Copy Markdown
Contributor

Just a little thing but I thought it was a nice lead-in to the next section, and would clear up a misconception if anyone tried to implement it themselves and inadvertently used the wrong order.

@Liable5607 Liable5607 changed the title remarked on changing order of (m + n) to (n + m) in drop' remarked on changing order of (m + n) to (n + m) in drop' in Section 6.3 Jul 20, 2025
@Liable5607 Liable5607 changed the title remarked on changing order of (m + n) to (n + m) in drop' in Section 6.3 Remark on changing order of (m + n) to (n + m) in drop' in Section 6.3 Jul 20, 2025
Comment thread src/Tutorial/Dependent.md Outdated
@stefan-hoeck stefan-hoeck merged commit 5252173 into stefan-hoeck:main Jul 21, 2025
2 checks passed
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