# Zulip Chat Archive

## Stream: new members

### Topic: How does `instantiate_vars` work?

#### Lucas Allen (Sep 03 2020 at 07:34):

Hola, in expr.lean there is the `instantiate_vars`

meta constant. The docs say

```
/-- ``instantiate_vars `(#0 #1 #2) [x,y,z] = `(%%x %%y %%z)`` -/
```

However, when I try

```
variables x y z : expr
#eval instantiate_vars `(#0 #1 #2) [x,y,z]
```

I get a red squiggle under the `#0`

and the error, "don't know how to synthesize placeholder

context". How do I get this to work?

#### Lucas Allen (Sep 03 2020 at 07:44):

If I try

```
variables x y z : expr
#eval instantiate_vars `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)) [x,y]
```

I get the error "cannot evaluate function: 0 arguments given but expected 2." I don't understand what's happening.

#### Reid Barton (Sep 03 2020 at 08:18):

What exactly are you trying to do? Something like your last example?

#### Reid Barton (Sep 03 2020 at 08:20):

``(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))`

is an `expr.pi`

, whose body is another `expr.pi`

, whose body is some other expression we'll call `e`

. If you called `instantiate_vars e [x,y]`

then you'd get an expression with `x`

and `y`

substituted for `a`

and `b`

, not sure in what order.

#### Lucas Allen (Sep 03 2020 at 08:27):

Yeah, basically given an expr I want to determine whether one of the leading `expr.pi`

's is a proposition. So for the example ``(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))`

I'd want false for the first two `expr.pi`

's and true for the last two. But when I try `infer_type`

it tells me to replace the variables with local constants.

#### Lucas Allen (Sep 03 2020 at 08:29):

I tried

```
meta def remove_pis : expr → expr
| (expr.pi var_name bi αₙ b) := remove_pis b
| e := e
#eval trace (remove_pis `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))
```

Which gives me "#3 ↔ #2", then

```
#eval instantiate_vars (remove_pis `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))) [x,y]
```

gives me a red squiggle under the `#eval`

and the error "cannot evaluate function: 0 arguments given but expected 2". I don't understand what this means and how to fix it.

#### Reid Barton (Sep 03 2020 at 08:30):

#mwe?

#### Lucas Allen (Sep 03 2020 at 08:30):

```
open tactic
open expr
meta def remove_pis : expr → expr
| (expr.pi var_name bi αₙ b) := remove_pis b
| e := e
#eval trace (remove_pis `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))
#eval instantiate_vars (remove_pis `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))) [x,y]
```

#### Rob Lewis (Sep 03 2020 at 08:36):

You're probably looking for https://leanprover-community.github.io/mathlib_docs/tactic/binder_matching.html

#### Lucas Allen (Sep 03 2020 at 08:40):

`open_pis`

might be what I want.

#### Lucas Allen (Sep 03 2020 at 08:40):

I'll check it out. Thanks.

#### Mario Carneiro (Sep 03 2020 at 13:44):

The notation `#0`

is sometimes used in the documentation to denote `expr.var 0`

, but there is no concrete syntax for this that the parser will accept

#### Lucas Allen (Sep 03 2020 at 21:32):

I think I forgot the variables in the MWE.

```
open tactic
open expr
meta def remove_pis : expr → expr
| (expr.pi var_name bi αₙ b) := remove_pis b
| e := e
variables x y z : expr
#eval trace (remove_pis `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))
#eval instantiate_vars (remove_pis `(∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b))) [x,y]
```

I feel bad about that.

#### Lucas Allen (Sep 03 2020 at 21:33):

Mario Carneiro said:

The notation

`#0`

is sometimes used in the documentation to denote`expr.var 0`

, but there is no concrete syntax for this that the parser will accept

Ok, so it's not possible to get the example in the docs to work.

Last updated: May 08 2021 at 10:12 UTC