Commit 2026-04-29 14:11 84c97f4a

View on Github →

chore(*): triage simpNF adaptation notes (#38468) This PR reinstates some @[simp] attributes that were removed due to various adaptation. At least if I run #lint in the files, the simpNF linter does not complain. So hopefully we should be able to add those lemmas to the simp set again.

Estimated changes