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

[Guillaume Allais]

Let me add that we have READMEs showing how to use these datatypes.
The AVL-tree one is using a strict total order based on propositional
equality but that's not the case for the Trie one:

https://agda.github.io/agda-stdlib/README.AVL.html
https://agda.github.io/agda-stdlib/README.Trie.NonDependent.html

On 27/04/2019 02:01, Matthew Daggitt wrote:
> 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
>>
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>