unexpected local in quotation expression

Stream: general

[Scott Morrison]

Simple expr question: how do I turn a nat into an expression?

[Scott Morrison]

I'm writing a tactic, I have an explicit nat argument, and I want to assertv some lemma, applied to that particular nat.

[Scott Morrison]

e.g. if n : expr, and a : nat, I tried writing to_expr `(trichotomy %%n a), but I get a "unexpected local in quotation expression" error at the a.

[Scott Morrison]

Curiously, the only search result for that error is that line in the source code.

[Chris Hughes]

This works for me.

meta def f (n : ℕ) (e : expr): expr :=
`(nat.add %%e %%`(n))

def g : ℕ := by tactic.exact (f 5 `(1))

#eval g

[Scott Morrison]

Thanks!

[Scott Morrison]

Documented at https://github.com/leanprover-community/mathlib/pull/786