Skip to content

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

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

Merged
stefan-hoeck merged 5 commits into from
Jul 21, 2025
Merged

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

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
6d11766
remarked on changing order of (m + n) to (n + m) in drop'
Liable5607 Jul 20, 2025
372db3a
trying to fix drop' duplication error
Liable5607 Jul 20, 2025
a59163a
it's actually the second xs
Liable5607 Jul 20, 2025
8af1bd0
trying to fix markdown error
Liable5607 Jul 20, 2025
0dd0974
changed quote to backticks and repl
Liable5607 Jul 21, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions src/Tutorial/Dependent.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -709,6 +709,15 @@ drop' 0 xs = xs
drop' (S k) (_ :: xs) = drop' k xs
```

Note that changing the order from `(m + n)` to `(n + m)`
in the second parameter will cause an error at the second `xs`:

```repl
While processing right hand side of drop'. Can't solve constraint between: plus n 0 and n.
```

You will learn why in the next section.

### Limitations

After all the examples and exercises in this section
Expand Down