[Agda] words

[Guillaume Allais]

Hi Philippe,

I've opened a PR on the standard library to add `wordsBy` and `words`.
https://github.com/agda/agda-stdlib/pull/1163

Cheers,
gallais

On 17/04/2020 07:44, Philippe de Rochambeau wrote:
> 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
> 
> 
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>