what is advantage of simprocs

Stream: general

[Asei Inoue]

From v4.6.0 simproc was introduced.
https://github.com/leanprover/lean4/releases/tag/v4.6.0

But what is 'newly' possible with the introduction of simproc? The examples given in the release notes seem to be sufficient for conventional simp.

[Asei Inoue]

What is newly possible with simproc in libraries such as mathlib?

[Alex J. Best]

One standard example of a simproc is that if the condition c in if c then h else h' simplifies to true then this can be replaced by just h before simp has a chance to simplify h' which is what it would normally do as it works bottom up.

[Asei Inoue]

simp made faster?

[Sebastian Ullrich]

https://lean-lang.org/blog/2024-2-29-lean-460/ has more examples