# Zulip Chat Archive

## Stream: metaprogramming / tactics

### Topic: to_expr failure

#### Markus Himmel (Jul 18 2020 at 12:20):

Hi, does anyone know what's going on in the following snippet?

```
lemma test (h : true) : true → true :=
λ h, trivial
lemma test' (h : 0 = 0) : true → true :=
λ h, trivial
meta def mk_test : tactic unit :=
do
e ← tactic.to_expr ``(test trivial),
tactic.to_expr ``(%%e trivial) >>= tactic.exact
meta def mk_test' : tactic unit :=
do
e ← tactic.to_expr ``(test' rfl),
tactic.to_expr ``(%%e trivial) >>= tactic.exact
lemma a : true :=
by mk_test -- works
lemma a' : true :=
by mk_test' -- function expected at `rfl` term has type `?m_2 = ?m_2`
```

In both cases, infering the type of `e`

gives `true → true`

as expected, but for some reason the second `to_expr`

fails in `mk_test'`

.

#### Rob Lewis (Jul 18 2020 at 15:13):

This definitely looks like a bug, one I don't remember seeing before. It seems like the elaborator is ignoring the `as_is`

annotation on `e`

.

#### Rob Lewis (Jul 18 2020 at 15:15):

For a bit more explanation: after ` e ← tactic.to_expr ``(test' rfl),`

`e`

is a fully elaborated expr. When you insert it into ```(%%e trivial)`

, which is a `pexpr`

, Lean knows that `e`

is already elaborated and makes a note of this. You can see the note if you `trace ``(%%e trivial)`

. When you elaborate that `pexpr`

it should know not to touch the thing inside this annotation.

#### Markus Himmel (Jul 18 2020 at 15:32):

Thank you for having a look at this. I have opened lean#395.

Last updated: May 09 2021 at 22:13 UTC