Antiquotes

Stream: new members

[Robert Maxton]

Allegedly, antiquotes are supposed to work in meta-tactic blocks like `[tac...]; but I'm getting invalid antiquotation, occurs outside of quoted expressions

[Robert Maxton]

Has this been changed since the tutorial was written?

[Yaël Dillies]

That still works. You probably need to give us more code for us to diagnose.

[Robert Maxton]

I'm doing something like

meta def tactic.interactive.restricted_induction (v: parse ident) (ax: parse ident): tactic unit :=
   `[revert %%v, apply ax, split]

[Robert Maxton]

where the idea is that I'm going to write down a bunch of different induction axioms of varying strength and use a specific one

[Yaël Dillies]

Isn't there anything below that line that could interfere?

[Robert Maxton]

and I'm not entirely sure I'm supposed to be using antiquotes in that situation in the first place lol

[Yaël Dillies]

I suspect adding #exit right after this line might solve your problem

[Robert Maxton]

hmmm
okay, that does fix the problem, but then how do I use the tactic lol

[Robert Maxton]

also I suspect it doesn't do what I need it to do anyway but to some extent that's a separate problem

[Yaël Dillies]

Fix whatever syntax error you introduced later :smile:

[Robert Maxton]

... that's kind of annoying, tbh

[Robert Maxton]

since that appears at the top of a namespace of half-finished theorems

[Robert Maxton]

oh well

[Robert Maxton]

anyway, I take that back, adding #exit doesn't actually remove the error anyway

[Robert Maxton]

I forgot to actually reintroduce the antiquote before checking last time >.>

[Robert Maxton]

still complains about antiquotations when I do

[Robert Maxton]

also the next line is namespace so I'd've been pretty surprised if that was the problem anyway

[Eric Wieser]

I think this doesn't work because revert expects a name not an expression.

[Eric Wieser]

And %% is for expressions

[Kyle Miller]

For example, this works:

import tactic

setup_tactic_parser

meta def tactic.interactive.restricted_induction (ax: parse texpr): tactic unit :=
   `[apply %%ax, split]

[Kyle Miller]

(but it doesn't solve using revert)

[Patrick Johnson]

This also works:

import tactic

section
setup_tactic_parser
open tactic.interactive

meta def tactic.interactive.restricted_induction
  (v : parse ident) (ax : parse texpr) : tactic unit := do
  revert [v], apply ax, split

end

[Patrick Johnson]

Example usage:

example {n : ℕ} (h : true ∧ true → ∀ {n : ℕ}, true) : true :=
begin
  restricted_induction n h,
  repeat { trivial },
end

[Robert Maxton]

hm. Okay, that's simpler than I had expected

[Robert Maxton]

In particular I was really scratching my head over how to make a many ident and it's a little embarrassing the answer was just "make a list of it" ^.^;

[Patrick Johnson]

parse ident* is definitionally equal to list name