Commit 2025-10-20 19:14 39996ca4
View on Github →feat(push): @[push] annotations for fun (#30038)
This PR adds the annotations for the tactics push fun _ ↦ _ and pull fun _ ↦ _ and the simprocs pushFun and pullFun.
The following operations are supported: 1, 0, *, +, ⁻¹, -, /, ^, •, +ᵥ, -ᵥ, star, ofNat, natCast, intCast, ⊔, ⊓, | |, ∆, ⇔, ⇨, ⊥, ⊤, ᶜ, \, default, algebraMap, kstar, ⌊/⌋, ⁺, ⁻, ⁺ᵐ, ⁻ᵐ.