See also examples/balanced_bst/balanced_mapTheory, which has a "fromList"
That does have the requirement of having the domain type capable of being


On Wed, Aug 7, 2019 at 3:45 AM Chun Tian (binghe) <>

> 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 mailing list

Reply via email to