The Coq mailing list

[Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>]

Hi Club,

I'm trying to understand the std library of finite maps. I would like

to have/define a function to construct the finite set of keys of

a finite map. This is what I have so far:

Set Implicit Arguments.
Require Import FMapInterface.
Require Import FMapList.
Require Import OrderedTypeEx.
Require Import FSetList.
Require Import MSetList.

Definition var := nat.
Definition var_eq  := Nat_as_OT.eq.
Definition var_dec := Nat_as_OT.eq_dec.

Module VarMap  := FMapList.Make Nat_as_OT.
Module VarFSet := FSetList.Make Nat_as_OT.
Module VarSet  := VarFSet.MSet.

Definition keys_list A (m : VarMap.t A) : list VarMap.key
  := map (@fst _ _) (VarMap.elements m).

(* how to implement this ??
Definition keys_set A (m : VarMap.t A) : VarSet.t
  := map (@fst _ _) (VarMap.elements m).
*)
 

Is there a way to "coerce" keys_list into a MSet ?

Any hint will be appreciated,
 
Thanks in advance,

Leo.