cadic.xyz / blog / coq_mset_tutorial /

Introduction

I'm using Coq for my masters thesis. I needed a notion of a set from set theory to formalize something. Unfortunatelly, Coq does not provide builtin sets. It has something called Set, but it's a notion used in the type system, and is used for something else than representing unordered groups of objects. Fortunately, sets can be found in the standard library of Coq. There are 3 options to choose from:

Unfortunatelly again, there are no tutorials for any of the preceding library modules. I wanted to change that, so the rest of the article contains a tutorial for listset, and for MSet.

listset

Exists, and is relatively easy to use.

MSet

Exists, but is not easy to use.

References