search

MarcelineVQ / idris2-bytes

ByteStrings for Idris2!
Other
7 stars 0 forks source link

add Strict.idr #1

Closed DSLstandard closed 3 years ago

DSLstandard commented 3 years ago

Version: Idris 2, version 0.2.1-aa6e36ef4

If src/Data/Bytes/Strict.idr doesn't exist, the following error will occur:

$ idris2 --install bytes.ipkg
Uncaught error: bytes.ipkg:14:11--15:1:Data.Bytes.Strict not found

Sidenote:

Sorry but honestly I'm not sure on how to make an appropriate response about the following problem:

In https://github.com/idris-lang/Idris2/commit/ef5299733a053c5c3ba92c99a2b5e07454ac2f0a, they've added <$ and $>, causing:

Error: While processing right hand side of $>. Ambiguous elaboration. Possible results:
    ?postpone [locals in scope: b, a, f, {conArg:506}]
    ?postpone [locals in scope: b, a, f, {conArg:506}]

src/Data/Bytes/Util.idr:88:13--88:17
    |
 88 | ($>) = flip (<$)
    |             ^^^^

It can be resolved by removing the definitions of <$ and $> in src/Data/Bytes/Util.idr. However, I don't know whether I should include it into this PR, make an issue, or wait until Idris2's next release (v0.2.2?).

MarcelineVQ commented 3 years ago

Oopsie, thank you, I do have that module but forgot to commit it, it's exactly what you've written :>

The error with $> is, I think, because recent idris2 has that as part of prelude now. I'll remove the Util version