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

TDDwI: Minor changes to chapter10 #3433

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Conversation

sagehane
Copy link
Contributor

@sagehane sagehane commented Dec 3, 2024

I hope this is the right place to suggest changes to https://idris2.readthedocs.io/en/latest/typedd/typedd.html.

While following the TypeDD book with idris2, I noticed that the code can be made total whilst resembling the original code more.

I checked the code with idris2 --check tests/typedd-book/chapter10/IsSuffix.idr but didn't run any tests because I didn't really understand how it works.


Unrelated, but I feel like it would be nicer if the Snoc constructor was changed from:

Snoc : (x : a) -> (xs : List a) -> SnocList xs -> SnocList (xs ++ [x])

to something better resembling idris1:

Snoc : {x : _} -> {xs : _} -> SnocList xs -> SnocList (xs ++ [x])

I assume there is a valid motivation for this change that I didn't catch, as I've never used Idris outside of the purposes of this book.

Note that the ``Snoc`` - ``Snoc`` case has to be written first otherwise Idris
generates a case tree splitting on ``input1`` and ``input2`` instead of the
``SnocList`` objects and this leads to a lot of cases being detected as missing.
``IsSuffix.idr`` also has to be adjusted to match the new ``Snoc`` arguments.
Copy link
Contributor Author

Choose a reason for hiding this comment

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

The comment probably can be improved. I'm especially confused as to why the new code doesn't need a | ysrec at line 300.

@sagehane
Copy link
Contributor Author

sagehane commented Dec 3, 2024

Also, assuming this is the right place to have this file edited, the link at

code is also [going to be] part of the test suite (see `tests/typedd-book
<https://github.com/edwinb/Idris2/tree/master/tests/typedd-book>`_ in the Idris
should probably be updated to this repo, instead of edwinb's repo.

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.

1 participant