Hello, I am creating an MSetList of Strings P, and I would like to obtain the Powerset of P. I am not being able to figure it out. Code below. Thanks for your help :slight_smile: Require Import Coq.MSets.MSetList Coq.Strings.String Coq.Structures.OrdersEx. Module set :…

The construction of set shows that you are using the Make function with a module as argument. If you type Print Make., you see that this is a functor taking a module of type OrderedType as argument, and it produces a module with many fields, among which t, eq, eq_equiv, lt, lt_strorder, lt_compat, c…

How to create a Powerset of MSetList?

Using Rocq

georgio February 24, 2022, 10:15am 3

Thank you very much!!

Topic		Replies	Views
Use a submodule of OrderedType in FSets Using Rocq	4	943	August 11, 2019
Finite sets (MSets) on dependent types Using Rocq	6	78	December 22, 2024
Extracting FSet and FMap to OCaml Using Rocq	2	643	March 4, 2020
Modules vs. generalized rewrite Using Rocq	4	573	September 19, 2022
Print Module [Type] lacks types Using Rocq	0	445	August 14, 2022

How to create a Powerset of MSetList?

Related topics