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 > email@example.com > https://lists.sourceforge.net/lists/listinfo/hol-info >
_______________________________________________ hol-info mailing list firstname.lastname@example.org https://lists.sourceforge.net/lists/listinfo/hol-info