Skip to content

Add set_omap to finite sets

Dorian Lesbre requested to merge dlesbre/stdpp:dorian/set_omap into master

Add omap-like function to finite sets, aka OCaml's filter_map operation.

I needed it to destruct a set of X + Y into a set of X and a set of Y.

Also add a few lemmas to reason about it.

Edited by Dorian Lesbre

Merge request reports