coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] MSet of keys of a FMap

From: CJ Bell <siegebell+coq AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] MSet of keys of a FMap
Date: Mon, 13 Apr 2015 22:26:04 -0400

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

Yes -- you should use of_list, defined in MSetProperties.

Require Import Coq.MSets.MSetProperties.
Module Props := MSetProperties.WProperties VarSet.

Definition keys_set {A} (m: VarMap.t A) : VarSet.t :=
Props.of_list (map (@fst _ _) (VarMap.elements m)).

(* you will probably find MSetFacts useful, too *)
Require Import Coq.MSets.MSetFacts.
Module Facts := MSetFacts.WFacts VarSet.

-cj

[Coq-Club] MSet of keys of a FMap, Leonardo Rodriguez, 04/14/2015
- <Possible follow-up(s)>
- Re: [Coq-Club] MSet of keys of a FMap, CJ Bell, 04/14/2015