TDDwI: Minor changes to chapter10

[sagehane]

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.

[sagehane]

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]

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

Idris2/docs/source/typedd/typedd.rst

Lines 10 to 11 in ecd6d47

	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.

[SlayerOfTheBad]

Whilst this solution works, it does not actually do what this example in Chapter 10 is meant to illustrate. This version does not recursively apply ysrec, which would lead to reduced performance, as the SnocList for ys needs to be constructed on each step.