Zulip Chat Archive

Stream: new members

Topic: Backtick anguish


view this post on Zulip Edward Ayers (Aug 16 2018 at 22:35):

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

view this post on Zulip Edward Ayers (Aug 16 2018 at 22:38):

Alternatively:

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

view this post on Zulip Simon Hudon (Aug 16 2018 at 22:39):

`(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)

view this post on Zulip Edward Ayers (Aug 16 2018 at 22:39):

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

view this post on Zulip Simon Hudon (Aug 16 2018 at 22:41):

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

view this post on Zulip Edward Ayers (Aug 16 2018 at 22:44):

This code still errors for me

view this post on Zulip Edward Ayers (Aug 16 2018 at 22:45):

unknown identifier 'q'

view this post on Zulip Edward Ayers (Aug 16 2018 at 22:46):

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

q : Prop
 Sort ?

view this post on Zulip Simon Hudon (Aug 16 2018 at 22:47):

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).


Last updated: May 16 2021 at 05:21 UTC