Commit 2025-12-01 17:54 2c2f5994
View on Github →feat: @[to_fun] attribute for generating fun _ => ... form of lemmas (#31872)
This PR shows that it is quite easy to have an attribute that generates a new declaration with fun pushed or pulled w.r.t. the original declaration.