Skip to content

chore: use non-deprecated iteratedFDeriv_fun_zero in ofDecayOn - #487

Merged
thefundamentaltheor3m merged 1 commit into
boundingfrom
claude/pr-review-audit-plan-n2a07a
Sep 29, 2026
Merged

thefundamentaltheor3m merged 1 commit into
boundingfrom
claude/pr-review-audit-plan-n2a07a

Conversation

@thefundamentaltheor3m

Copy link
Copy Markdown
Owner

Follow-up to #485. CI on #460 (head cce794e) is green but reports:

warning: SpherePacking/ForMathlib/RadialSchwartz/Multidimensional.lean:56:49: `iteratedFDeriv_zero_fun` has been deprecated: Use `iteratedFDeriv_fun_zero` instead

This swaps in the suggested replacement (a one-token change; the deprecated name is an alias of it).

🤖 Generated with Claude Code

https://claude.ai/code/session_01UXLVscFdDj42KSSxpVWBHP


Generated by Claude Code

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UXLVscFdDj42KSSxpVWBHP
@thefundamentaltheor3m
thefundamentaltheor3m marked this pull request as ready for review September 29, 2026 14:39
@thefundamentaltheor3m
thefundamentaltheor3m merged commit 17b3ead into bounding Sep 29, 2026
@thefundamentaltheor3m
thefundamentaltheor3m deleted the claude/pr-review-audit-plan-n2a07a branch September 29, 2026 14:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants