Commit 2025-02-03 07:17 da0385c6

View on Github →

chore(Logic/Equiv): change type of sumEquivSigmaBool to simp normal form (#21338) simp eagerly rewrites Bool.casesOn to Bool.rec, so using the former in the type signature prevents related simp lemmas from firing. See Zulip discussion.

Estimated changes