Document moved SplitRec View to contrib #3493
Conversation
In Idris2, `Data.Vect.Views` from the `base` library has been moved to `Data.Vect.Views.Extra` in the `contrib` library. This has so far remained undocumented in TDDwI: Changes Required.
docs/source/typedd/typedd.rst
Outdated
| For the ``SplitRec`` view in the exercise 2 after Chapter 10-2, ``import Data.Vect.Views.Extra`` from ``contrib`` library. | ||
|
|
||
| For the ``VList`` view in exercise 4 after Chapter 10-2, ``import Data.List.Views.Extra`` from ``contrib`` library. |
There was a problem hiding this comment.
Why?
in the exercise 2
but
in exercise 4
There was a problem hiding this comment.
I must've copy-pasted the exercise 4 line, then deleted the the in the line about exercise 4 and forgot to in the exercise 2 line. Fixed.
|
I'd also accept a PR that moved us in the direction of disbanding this part of contrib since that's the end goal, but with no time horizon on that I think the documentation is a good addition 👍. |
|
Except for the fact that your documentation appears to be inaccurate. I see SplitRec in the base library if I'm not mistaken. |
|
Oh. Oh no. I see now that I was looking at List. So for lists the SplitRec view is in base and for Vect it is in contrib. That's plenty reason to move the Vect view into base if you ask me. I suppose this documentation change is acceptable but would you be open to migrating that Extra module into base instead? |
|
I would be open to migrating it, I had just assumed there was some reason for If it is merely a matter of moving the files over and updating module names, I'll gladly do it. But if there is work to be done on the implementation (soundness proofs or whatever), I am not confident enough in my Idris nor Type Theory to undertake that at the moment. 😅 |
|
Go ahead and do the easy thing. I’ll sanity check the code but we can also fix any bugs in it in the future regardless. |
|
@mattpolzin I've moved |
In Idris2,
Data.Vect.Viewsfrom thebaselibrary has been moved toData.Vect.Views.Extrain thecontriblibrary. This has so far remained undocumented in TDDwI: Changes Required.