Def Tactic.higherOrderGetParam

Modification history

2026-07-16 01:47
Mathlib/Tactic/HigherOrder.lean
chore: bump toolchain to v4.33.0-rc1 (#41779)
Deleted Tactic.higherOrderGetParamView on Github →
2023-03-08 10:44
Mathlib/Tactic/HigherOrder.lean
feat: port higher_order attribute (#2438)
Added Tactic.higherOrderGetParamView on Github →