Commit 2024-04-15 06:46 7eeaaffb
View on Github →chore: classify porting notes about additional necessary beta reduction (#12130) This subsumes some of the notes in #10752 and #10971. I'm on the fence as to whether replacing the dsimp only by beta_reduce is useful; this is easy to revert if needed.