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: Dec 20 2023 at 11:08 UTC