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
true → true as expected, but for some reason the second
to_expr fails in
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
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