[Agda] Fwd: [External] Re: Example of Finite maps with an string keys?

[Matthew Daggitt]

Note that the StackOverflow links given by Orestis are a little out of
date, as AVL trees in the standard library v1.0 now support arbitrary
equalities. There's also a Trie implementation been added to the
development version of the standard library as of last week.

Matthew

On Sat, Apr 27, 2019 at 5:02 AM Aaron Stump <aaron-stump at uiowa.edu> wrote:

> You might also be interested in the trie data structure in the Iowa Agda
> Library:
>
> https://github.com/cedille/ial/blob/master/trie.agda
>
> Best,
> Aaron
>
> On 4/26/19 12:45 PM, Orestis Melkonian wrote:
>
> You can find examples here:
>
> 1. (SO)
> https://stackoverflow.com/questions/36269333/agdas-standard-library-data-avl-sets-containing-data-string-as-values
> 2. (SO)
> https://stackoverflow.com/questions/42614042/map-with-strings-as-keys-in-agda
> 3. (Gist) https://gist.github.com/gallais/358ba798323868a7c4e0
>
> Cheers,
> --OM
>
> On 26-04-19 19:04, Serge Leblanc wrote:
>
> Dear All, does someone haves an example of AVL trees with String-type
> keys?
>
> Saluton, ĉu iu havas 'AVL-trees'-ekzemplon kun String-tipa klavo?
> Sinceran dankon pro via helpo.
>
> --
> Serge Leblanc
> ------------------------------
> gpg --search-keys 0x67B17A3F
> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190427/29c7e68f/attachment.html>