Qq function application

Stream: metaprogramming / tactics

[Moritz Doll]

If I have a function f how do I qq-match against its application? I've tried variants of the code below, but nothing worked and I couldn't find an example in mathlib

import Lean
import Qq

open Lean Meta Qq

set_option autoImplicit true

variable {α : Q(Type u)}

def test (f : Q($α → $α)) (e : Q($α)) : MetaM Unit := do
  match e with
  | ~q($f $a) =>
    pure ()
  | _ => pure ()

[Eric Wieser]

~q matching, just like any other matching, doesn't let you match against things in the local context.

[Eric Wieser]

This works:

def test (f : Q($α → $α)) (e : Q($α)) : MetaM Unit := do
  let a ← mkFreshExprMVarQ q($α)
  if let .defEq h ← isDefEqQ q($e) q($f $a) then
    pure ()
  else
    pure ()

[Eric Wieser]

Though there is probably a trap there with metavariable depths