Commit 2025-12-02 20:43 04dff12e
View on Github →feat: add missing push attributes for @[to_fun] (#32341)
This PR add two missing push tags for the pull fun _ ↦ _ tactic used by @[to_fun].
feat: add missing push attributes for @[to_fun] (#32341)
This PR add two missing push tags for the pull fun _ ↦ _ tactic used by @[to_fun].