Backtick anguish

Stream: new members

[Edward Ayers]

What am I doing wrong here?

meta def my_tactic (q : Prop) : tactic unit :=
  do
  define `qq `(q)

failed to synthesize type class instance for
q : Prop,
my_tactic : tactic unit
⊢ reflected q

[Edward Ayers]

Alternatively:

open tactic
def my_lemma (q : Prop) : q :=
begin
  define_core `qq `(q),
  sorry
end

unknown identifier 'q'

[Simon Hudon]

`(q) is used to build expr values but its type is actually reflected q. This is a long way of saying that Lean is trying to convert a known value into an expression. Because q is a local variable, its value is not know and cannot be reflected. You need to go through to_expr ``(q)

[Edward Ayers]

I want to pass the local_const with the pretty name "q" as the type arg to define_core

[Simon Hudon]

Your code could be adapted into the following:

open tactic
def my_lemma (q : Prop) : q :=
begin
  (do my_q <- to_expr ``(q), define_core `qq my_q),
  sorry
end

or, more concisely:

open tactic
def my_lemma (q : Prop) : q :=
begin
  (to_expr ``(q) >>= define_core `qq),
  sorry
end

[Edward Ayers]

This code still errors for me

[Edward Ayers]

unknown identifier 'q'

[Edward Ayers]

invalid define tactic, expression is not a type
  ⁇
state:
2 goals
q : Prop
⊢ q

q : Prop
⊢ Sort ?

[Simon Hudon]

Oh! I see why. Use (to_expr ```(q) >>= define_core `qq): q is not available in the scope of your tactic code. With three ticks, you're disabling scope checking when compiling that tactic. Equivalently, you can do (get_local `q >>= define_core `qq).