Hi Konrad,
thanks for pointing me to balanced_mapTheory, where I found some useful
LIST_REL related theorems, but the "fromList" is not what I can use.
After another look into listTheory, I think my previous alist built by MAP2 can
be also done by ZIP. So I'm going to use ZIP for now.
--Chun
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)
wrote:
> Hi,
>
> I wonder what's the most natural/native way to
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))
