[Agda] words

[Philippe de Rochambeau]

Hello,

does anyone how to implement Idris’s ‘words’ function in Agda?

I couldn’t find it in Agda Builtins, neither could I find ‘unpack’.

https://github.com/idris-lang/Idris-dev/blob/713e485ff6d35f11b1e29b20388d02ff5c43d0db/libs/prelude/Prelude/Strings.idr <https://github.com/idris-lang/Idris-dev/blob/713e485ff6d35f11b1e29b20388d02ff5c43d0db/libs/prelude/Prelude/Strings.idr>

Many thanks.

Cheers,

Philippe




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200417/97be17be/attachment.html>