Commit 2024-11-25 13:34 3fa5f452

View on Github →

chore: ensure there is a replacement identifier or text suggestion for all deprecations (#19426) This is for compatibility with the stricter requirements of leanprover/lean4#6112. Anyone is welcome to replace the "No deprecation message was provided." messages in other PRs! :-)

Estimated changes

modified theorem List.sublist_join
modified theorem List.pairwise_map'
modified def Combinator.I
modified def Combinator.K
modified def Combinator.S
modified theorem Classical.cases_true_false