how does one get a `higher_order` annotation in Lean 4?

Stream: mathlib4

[Arien Malec]

I see the Mathport.Syntax definition and tried to import that, but got nothing...

[Arien Malec]

Also tried to follow the breadcrumbs up from Mathport.Syntax & get unknown attribute [higherOrder]

[Mario Carneiro]

things in Mathport.Syntax represent syntax for tactics and annotations that have not yet been implemented

[Arien Malec]

OK -- so control.bifunctor is blocked, or I can hand-roll what's needed.

If I understood the Lean 3 implementation, the goal is to take theorem foo ∀ x, f (g x) = h xand reason over theorem foo_f_g: f ∘ g = h...