## 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