Commit 2023-10-17 06:25 2da494d2

View on Github →

chore: swap primes on forall_apply_eq_imp_iff (#7705) Two pairs of the form foo and foo', where foo' is the simp lemma (and hence used in many simp onlys) and foo is not used at all. Swap the primes, so that when it is time (now!) to upstream the lemma we actually use, it doesn't need to have a prime...

Estimated changes