## Stream: metaprogramming / tactics

### Topic: finding terms of a certain type in a expr

#### Eric Wieser (Feb 28 2021 at 17:59):

How can I write a function that detects if a (fully-elaborated) expr contains a certain type? For example, I want contains_nat (1 + 1 > 0) to give tt, but contains_nat (tt)  to give ff.

#### Alex J. Best (Feb 28 2021 at 18:06):

I think we have docs#expr.contains for this. If you wanted to write it you would fold over the expr, oops I'm on mobile and that link doesn't work sorry

#### Eric Wieser (Feb 28 2021 at 18:07):

Even without folding, I can't find the API to ask for the elaborated type of an expression

#### Yakov Pechersky (Feb 28 2021 at 18:07):

Would infer_type help here?

#### Eric Wieser (Feb 28 2021 at 18:16):

That's certainly what I was looking for, although it seems not to be enough:

private meta def decidable_exact (d : declaration) : tactic (option string) :=
do (binders, body) ← open_pis d.type,
body.mfold none $λ e depth so_far, do t ← infer_type e, if t.is_app_of decidable_eq ∨ t.is_app_of decidable_pred ∨ t.is_app_of decidable_rel ∨ t.is_app_of decidable then do trace t else skip, pure (some ("ok")) lemma bad {α : Type*} [inhabited α] [decidable_eq α] (x : α × α) : 0 = if x = default _ then 0 else 0 := sorry run_cmd do d ← get_decl bad, x ← decidable_exact d, trace x  gives tactic 'infer_type' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic  #### Yakov Pechersky (Feb 28 2021 at 18:48): How about this? private meta def decidable_exact (d : declaration) : tactic (option string) := do (binders, body) ← open_pis d.type, body.mfold none$ λ e depth so_far, do
if (e.get_free_var_range = 0) then (do
t ← infer_type e,
if t.is_app_of decidable_eq
∨ t.is_app_of decidable_pred ∨ t.is_app_of decidable_rel
∨ t.is_app_of decidable then do
trace t
else skip)
else skip,
pure (some ("ok"))

lemma bad {α : Type*} [inhabited α] [decidable_eq α] (x : α × α) :
0 = if x = default _ then 0 else 0 :=
sorry

run_cmd do
x ← decidable_exact d,
trace x


#### Eric Wieser (Feb 28 2021 at 18:54):

Does docs#expr.get_free_var_range reveal anything?

#### Yakov Pechersky (Feb 28 2021 at 18:57):

I'm just using is to filter out the expressions where the de Brujin var is behind a lambda

#### Floris van Doorn (Mar 02 2021 at 17:17):

Are you just looking for docs#expr.contains_constant?

#### Floris van Doorn (Mar 02 2021 at 17:18):

You cannot use infer_type in an expr.mfold, since the subexpressions are not well-typed (they could contain free de Bruijn variables).

#### Eric Wieser (Mar 02 2021 at 17:22):

contains_constant wouldn't return true for contains_constant (f x y) {nat} right? even if x has type nat?

#### Floris van Doorn (Mar 03 2021 at 18:56):

If f has type nat -> ... then no. However, for something like (1 + 1 > 0) you would get true, since has_lt is applied to nat.

One solution is to mfold over the expression:

• If you see nat it contains nat
• If you reach a local constant, use infer_type on it (which is safe, since it's a local constant) to see whether its type contains nat
• If you reach a constant, use docs#environment.get and docs#declaration.type to see whether its type contains nat`.

This should cover all cases.

#### Floris van Doorn (Mar 03 2021 at 18:57):

Except maybe some macros...

Last updated: May 09 2021 at 23:10 UTC