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>
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
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
