# Re: [Hol-info] How to express a finite_map or alist using a key list and a value list?

```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:
> construct.
> That does have the requirement of having the domain type capable of being
> ordered.
>
>
>
> 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
```