Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Match function application


Yaël Dillies (Aug 24 2022 at 09:21):

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 (Aug 24 2022 at 09:36):

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

Anne Baanen (Aug 24 2022 at 11:54):

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

Yaël Dillies (Aug 24 2022 at 12:35):

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 (Aug 24 2022 at 13:41):

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

Yaël Dillies (Aug 24 2022 at 13:51):

The instance parameter is not part of the match.


Last updated: Dec 20 2023 at 11:08 UTC