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