Match function application

Stream: metaprogramming / tactics

[Yaël Dillies]

I want to match something of the form f a where f : seminorm 𝕜 E (docs#seminorm). I can match f alone using `(⇑%%f) but how do I match the function application?

[Yaël Dillies]

Figured it out! I needed expr.app `(⇑%%f) `(%%a). Feel free to tell me if there's something more idiomatic.

[Anne Baanen]

Does `(⇑%%f %%a) not work?

[Yaël Dillies]

meta def positivity_seminorm : expr → tactic strictness
| `(⇑%%f %%a) := nonnegative <$> mk_app ``map_nonneg_add [f, a]
               <|> nonnegative <$> mk_app ``map_nonneg_mul [f, a]
| _ := failed
/-
function expected at
  ⇑_x_1
term has type
  ?m_1 _x_1
-/

(MWE on #16228)

[Eric Wieser]

Does `(⇑%%f) match a specific coe_to_fun or is the instance parameter not part of the match?

[Yaël Dillies]

The instance parameter is not part of the match.