Commit 2025-03-17 00:33 5e56bc5f
View on Github →fix: missing simp lemmas for bundled coercions (#22984)
Most of the time simps does too much here but simps -fullyApplied does too little, so we have to write them manually.
fix: missing simp lemmas for bundled coercions (#22984)
Most of the time simps does too much here but simps -fullyApplied does too little, so we have to write them manually.