Skip to content

[ add ] Data.Vec.Recursive.Relation.Binary.Pointwise - #3110

Open
jkopanski wants to merge 1 commit into
agda:masterfrom
jkopanski:master
Open

[ add ] Data.Vec.Recursive.Relation.Binary.Pointwise#3110
jkopanski wants to merge 1 commit into
agda:masterfrom
jkopanski:master

Conversation

@jkopanski

Copy link
Copy Markdown
Contributor

Recently I've came across Data.Vec.Recursive which seemed interesting enough for me to play with it. However there is lackluster support for it. So I thought this would be some grunt work that I could contribute to the library. Everything here is pretty mechanical translation from
Data.Vec.Relation.Binary.Pointwise.Inductive with only splitAt being included for completeness. I couldn't get append because of the indices _+ 0. Perhaps when I add cast next this would budge.

Recently I've came across `Data.Vec.Recursive` which seemed
interesting enough for me to play with it.  However there is
lackluster support for it.  So I thought this would be some grunt work
that I could contribute to the library.  Everything here is pretty
mechanical translation from
`Data.Vec.Relation.Binary.Pointwise.Inductive` with only `splitAt`
being included for completeness.  I couldn't get `append` because of
the indices `_+ 0`.  Perhaps when I add `cast` next this would budge.
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