Commit 2026-03-26 22:21 5a8998f5

View on Github →

chore(Logic): deprecate forall_swap and exists_swap (#37164) This PR deprecates the lemmas forall_swap and exists_swap, which are duplicates of the lemmas forall_comm and exists_comm in Init.PropLemmas. I prefer the _comm names, and the number of usages of _comm is noticeably higher than _swap in the library. Also rename forall₂_swap to forall₂_comm for consistency.

Estimated changes

deleted theorem exists_swap
deleted theorem forall_swap
added theorem forall₂_comm
deleted theorem forall₂_swap