Skip to content

Add cartesian products to all concrete set types

Thibaut Péramirequested to merge
tperami/stdpp:cprod into master

This adds a set Cartesian product on:

  • list
  • gset
  • propset
  • boolset
  • listset

With the notation A × B at level 37. The notation is left associative so that lA × lB × lC : list (A * B * C). This includes corresponding specification lemmas and SetUnfoldElemOf instances. I only did a set level specification. There is no lemma in this MR describing the order for the Cartesian product on lists (the only one of those types where order is relevant)

Merge request reports