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?


Attachment: signature.asc
Description: OpenPGP digital signature

hol-info mailing list

Reply via email to