Commit 2023-03-08 10:44 c63372cc

View on Github →

feat: port higher_order attribute (#2438)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Tactic/HigherOrder.lean

added def Tactic.higherOrderGetParam

added def Tactic.mkComp

Created test/HigherOrder.lean

added theorem HigherOrderTest.map_pure'