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