## Stream: general

### Topic: get the "visible" head of an expression

#### Scott Morrison (Mar 11 2021 at 23:19):

I would like a function that takes an expr, and returns to me the "head", including implicit arguments.

Thus @rfl X should stay as @rfl X, nat.factorial 7 should produce nat.factorial, and 3 + 7 should produce @has_add.add nat nat.has_add.

#### Scott Morrison (Mar 11 2021 at 23:19):

Does that make sense? Do we already have it?

#### Scott Morrison (Mar 11 2021 at 23:20):

There is expr.get_app_fn, which gets the very topmost head of the app. (But this turns @rfl X into just @rfl, etc.)

#### Scott Morrison (Mar 11 2021 at 23:25):

I guess if it existed it would be in src/meta/expr.lean, and there doesn't seem to be anything like this.

#### Scott Morrison (Mar 11 2021 at 23:30):

I had hoped that I could achieve this using pattern matching, e.g. something like

match e with
| (%%f %%x) := return f
| _ := sorry
end


but this just gives me a function expected at error on the %%f.

#### Scott Morrison (Mar 12 2021 at 00:28):

meta def app_implicits : expr → list expr → tactic expr
| f [] := return f
| f (x :: xs) := do
ty ← infer_type f,
match binding_info ty with
| binder_info.default := return f
| _ := app_implicits (f x) xs
end

meta def get_app_fn_with_implicits (e : expr) : tactic expr :=
do
let (f, args) := e.get_app_fn_args,
app_implicits f args


seems to do it.

#### Mario Carneiro (Mar 12 2021 at 02:38):

Here's a version that avoids multiple calls to infer_type:

import tactic.core
open tactic expr

meta def app_implicits : expr → list expr → expr → expr
| f (x :: xs) (pi _ binder_info.default _ ty) := f
| f (x :: xs) (pi _ _ _ ty) := app_implicits (f x) xs ty
| f _ _ := f

meta def get_app_fn_with_implicits (e : expr) : tactic expr :=
let (f, args) := e.get_app_fn_args in
app_implicits f args <\$> infer_type f
`

#### Scott Morrison (Mar 12 2021 at 10:47):

Thanks!

Last updated: May 13 2021 at 21:12 UTC