Commit 2023-12-22 20:59 21e45c8b

View on Github →

chore(Set/NAry): drop Set.image3 (#9221) Set.image3 was only used to prove associativity of Set.image2. It had basically no API and had exactly one (easily replaced) use outside Data.Set.NAry). There is no specific function as a replacement, but it can be obtained by combining Set.image2 twice.

Estimated changes

deleted theorem Set.image2_image2_left
deleted theorem Set.image2_image2_right
deleted def Set.image3
deleted theorem Set.image3_congr'
deleted theorem Set.image3_congr
deleted theorem Set.image3_mono
deleted theorem Set.mem_image3