Commit 2026-09-28 05:55 0c51c7e4

View on Github →

chore: remove some backward.isDefEq.respectTransparency.instanceSearchTypes (#44157) This PR removes some of the recently introduced backward.isDefEq.respectTransparency.instanceSearchTypes options, using a simple fix. In some cases the problematic lemma has been removed entirely because it was added as a simp normal form variant of another lemma, but that other lemma is already in simp normal form. By the way, each of these has a long AI explanation of the failure that is not super helpful.

Estimated changes