Hi Konrad, thanks for pointing me to balanced_mapTheory, where I found some useful LIST_REL related theorems, but the "fromList" is not what I can use.
After another look into listTheory, I think my previous alist built by MAP2 can be also done by ZIP. So I'm going to use ZIP for now. --Chun Il 07/08/19 20:05, Konrad Slind ha scritto: > See also examples/balanced_bst/balanced_mapTheory, which has a "fromList" > construct. > That does have the requirement of having the domain type capable of being > ordered. > > Konrad. > > > On Wed, Aug 7, 2019 at 3:45 AM Chun Tian (binghe) <binghe.l...@gmail.com > <mailto:binghe.l...@gmail.com>> wrote: > > Hi, > > I wonder what's the most natural/native way to express a finite_map or > alist, using a key list and a value list (assuming their lengths are the > same, and the key list is all distinct)? > > My current idea is to use MAP2 to build an alist of type ``:('a # 'b) > list``: > > MAP2 (\k v. (k,v)) (ks :'a list) (vs :'b list) > > then (if needed), `alist_to_fmap` will lead me to a finite_map. But > shouldn't it be already provided by a definition in alistTheory (or > finite_mapTheory) that I just didn't find out? > > --Chun > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> > https://lists.sourceforge.net/lists/listinfo/hol-info >
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
