quotations and expr

Stream: general

[Fabian Glöckle]

Hello, I am new to metaprogramming and am stuck at the following:
I want to create a declaration which depends on a given name variable, like the following:

meta def my_easy_decl (x : name) : declaration :=
mk_definition `my_def [] `(ℕ) (const x [])

Because my intended term is more complicated than this MWE, I was hoping to achieve the same result with reflection along the lines of

meta def my_easy_decl' (x : name) : declaration :=
mk_definition `my_def [] `(ℕ) `(%%x)

Because declarationneeds an expr(not expr ff), I cannot use double backtick quotation. Single backtick quotation and %%as above yield

type mismatch at application
  expr.subst `(λ (_x_1 : ?_mlocal._fresh.3030.69), _x_1)
term
  `(λ (_x_1 : ?_mlocal._fresh.3030.69), _x_1)
has type
  reflected (λ (_x_1 : ?m_1), _x_1)
but is expected to have type
  expr

[Mario Carneiro]

The notation `(%%x) doesn't make sense since that expects x to have type expr rather than name. It's not clear what you are aiming for here that isn't achieved by the first version

[Mario Carneiro]

In all likelihood, you will need to use mk_const and/or to_expr to turn your pexprs into exprs, and this will require my_easy_decl to be a tactic

[Fabian Glöckle]

Thanks. I am aiming for an equivalent of the first version which does not force me to write a huge expr term in terms of nested constructors (because the const x [] will just be a part of it).

meta def my_easy_decl' (x : name) : tactic declaration :=
do cx ← mk_const x,
   mk_definition `my_def [] `(ℕ) (to_expr ``(%%cx))

[Fabian Glöckle]

Now the problem is that the last term is a tactic exprwhich mk_definitionwon't accept.

[Johan Commelin]

@Fabian Glöckle Have you seen https://github.com/leanprover-community/mathlib/blob/master/docs/extras/tactic_writing.md#marios-backtick-cheat-sheet? I guess it might be useful.

[Fabian Glöckle]

Ah great, thanks!

[Fabian Glöckle]

... which taught me both quotation and monads.
The following worked:

meta def my_easy_decl (x : name) : tactic declaration :=
do cx ← mk_const x,
  body ← to_expr ``(%%cx),
  pure $ mk_definition `my_def [] `(ℕ) body

Thanks both of you!